Induction Principles Formalized in the Calculus of Constructions

15 years 26 days ago

Download yquem.inria.fr

The Calculus of Constructions is a higher-order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn [2, 3], Girard [12], Martin-L

Gérard P. Huet

Real-time Traffic

Calculus | General Induction Schema | Induction Schema | Software Engineering | TAPSOFT 1987 |

claim paper

» From formal proofs to mathematical proofs a safe incremental way for building in firstorde...

» Engineering formal metatheory

» Polyhedra genus theorem and Euler formula A hypermapformalized intuitionistic proof

» Nominal System T

» Map fusion for nested datatypes in intensional type theory

» Pi an Interactive Derivation Editor for the Calculus of Partial Inductive Definitions

» A Few Constructions on Constructors

» Reasoning about Objectbased Calculi in CoInductive Type Theory and the Theory of Contexts

Post Info
More Details (n/a)

Added	28 Aug 2010
Updated	28 Aug 2010
Type	Conference
Year	1987
Where	TAPSOFT
Authors	Gérard P. Huet

Comments (0)

Sciweavers

Induction Principles Formalized in the Calculus of Constructions

Calculus | General Induction Schema | Induction Schema | Software Engineering | TAPSOFT 1987 |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers