Project Tags: Type Theory

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…