6 papers
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Matthew Bolan, Joachim Breitner, Jose Brox +31
We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project suc…
Formal Methods for the Informal Engineer: Workshop Recommendations
Gopal Sarma, James Koppel, Gregory Malecha +5
Formal Methods for the Informal Engineer (FMIE) was a workshop held at the Broad Institute of MIT and Harvard in 2021 to explore the potential role of verified software in the biom…
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong +1
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring inform…
A heuristic prover for real inequalities
Jeremy Avigad, Robert Y. Lewis, Cody Roux
We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem provin…
Refinement Types as Higher Order Dependency Pairs
Cody Roux
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of…
On the relation between size-based termination and semantic labelling
Frédéric Blanqui, Cody Roux
We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expr…