Formalisations by the Programming Systems Lab

Saarland University Computer Science
Coq Library of Undecidability Proofs

The Coq Library of Undecidability Proofs contains machine-checked reductions to establish undecidability results in Coq. The undecidability proofs are based on a synthetic approach to undecidability.

Set Theory Formalizations in Coq

The lab has done a number of set theory related formalizations in Coq including constructions of models of set theory and constructions of models of type theory using set theory.

A Constructive Theory of Regular Languages

We present a formal constructive theory of regular languages in Coq+Ssreflect. The development includes Kleene's Theorem, the Myhill-Nerode Theorem and a number of other constructions.

A Semantics for Intuitionistic Extensional Higher-Order Logic Supporting Higher-Order Abstract Syntax

We formalize a higher-order logic with Church style typing. We also formalize an M-set model where the monoid M is a type of substitutions and a base type is interpreted as untyped lambda terms. This M-set model justifies representing untyped lambda terms using higher-order abstract syntax in the higher-order logic. The Autosubst package is used to support reasoning about substitutions and terms.

Heyting Algebras and Kripke Models

We formalize two well-known semantics for intuitionistic propositional logic: Heyting algebras and Kripke models. We prove both semantics are sound for an intuitionistic propositional logic with only implication and false. We use Heyting algebras to prove undefinability results. We also prove a Kripke model can be converted into a Heyting algebra. Assuming excluded middle, we can convert a Heyting algebra into a Kripke model. In some ways our task is made easier by the fact that the logic does not have disjunction.

Finite Sets over Countable Types in Ssreflect

We develop a library for finite sets using Ssreflect. In contrast to the "finset" library in Ssreflect, which only allows finite base types, we allow countable types as base types. Finite sets are implemented as a quotient on lists using some canonical duplicate free list as representative. We provide most of the basic theory as well as constructions for least and greatest fixpoints and maximal extensions.

Legal notice, Privacy policy