European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

In the International School on Logical Frameworks and Proof Systems Interoperability.

Lecturer: Frédéric Blanqui

In this course, we are going to see how dependent types and rewriting rules (aka oriented equations) can be used to represent the proofs of various logical systems, so as to facilitate their exchange between provers. In a practical session, we will learn how to use the interactive logical framework Lambdapi, which implements the λΠ-calculus modulo rewriting. Finally, we will see how to try to automatically check some important properties of the rewrite systems one can define in Lambdapi.

Outline:

  1. Introduction to proof systems interoperability, λ-calculus and dependent types.

    (To prepare the practical session tomorrow, please install Lambdapi on your machine.)

  2. Introduction to pure type systems, rewriting, λΠ/R and the Lambdapi proof assistant. Practical session on Lambdapi.

  3. Encoding logics in λΠ/R: first-order logic, polymorphism, higher-order logic, pure type systems, …

  4. Properties of λΠ/R: decidability of type-checking, subject-reduction, confluence, termination, dependencies between these properties.