Project Tags: Formal Verification

Automating the Meta-Theory of Proof Systems

Proving properties about proof systems is a necessary task to make sure that they are sound and satisfy basic criteria for the application being considered. Nevertheless, it is a tedious…

Reimplementing Dependent Pattern Matching and Termination Checking in the Coq Theorem Prover

Coq is an interactive proof assistant (theorem prover) based on a long-studied dependent Type Theory called the Calculus of (Co-)Inductive Constructions (CIC). It is a mature system that has been…