Search

• < Previous
• 1
• Next >

---

The computability path ordering

Frédéric Blanqui ; Jean-Pierre Jouannaud ; Albert Rubio.

This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version,&nbsp;[&hellip;]

---

A modular construction of type theories

Frédéric Blanqui ; Gilles Dowek ; Emilie Grienenberger ; Gabriel Hondet ; François Thiré.

The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of U corresponding to each of these systems, and&nbsp;[&hellip;]

---

Sharing proofs with predicative theories through universe-polymorphic elaboration

Thiago Felicissimo ; Frédéric Blanqui.

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics to proof&nbsp;[&hellip;]

---