scientific article

From MaRDI portal

Publication:3030827

Jump to:navigation, search

zbMath0627.03045MaRDI QIDQ3030827

Gérard Huet, Thierry Coquand

Publication date: 1987

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Curry-Howard isomorphism intuitionistic type theory Automath interactive proof system calculus of construction formalisation of higher-order natural deduction

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Proof theory and constructive mathematics (03F99)

Related Items

Variants of the basic calculus of constructions ⋮ The calculus of constructions ⋮ Programming with streams in Coq a case study: The Sieve of Eratosthenes ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ On the proof theory of Coquand's calculus of constructions ⋮ Synthesis of ML programs in the system Coq

Uses Software

Automath

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:3030827&oldid=16062782"