H ? « ‹ ← → › »

Language peer sets for coq:
France↑
France/1991↑
Designed 1991 ↑
1990s languages ↑
Fifth generation↑
Post-Cold War↑
String and List Processing ↑
String and List Processing/1991↑
String and List Processing/fr ↑

coq(ID:6970/)

alternate simple view
Country: France
Designed 1991
Sammet category: String and List Processing

inductive proof system

for Calculus of Constructions (but also for T Coquand who created the Coc, and of course the Rooster being the symbol of France etc)

A higher-order proof system based on the Curry-Howard(-deBruijn) isomorphism between propositions and types, proofs and terms in a pure functional language. By restraining to constructive logic (i.e. no built-in choice axiom) it allows to extract actual programs from proofs. But, it is not reflective, and there's no way to meta-translate expressions.
Related languages
AUTOMATH → coq   Based on
coq → ALF   Based on
coq → Gallina   Subsystem
coq → LEGO   Based on
References:
  • (1991) Dowek, G.; Felty, A.; Herbelin, H.; Huet, G.; Paulin-Mohring, C. and B. Werner. "The COQ Proof Assistant User's Guide" Version 5.6. Rapports Techniques 134, INRIA, 1991
  • (1993) Coq User's Guide INRIA Rapport Technique No 154, Mai 1993
  • Cerioli et al (1997) Cerioli, Maura; Gogolla, Martin; Kirchner, Helene; Bruckner, Bernd Krieg; Qian, Zhenyu; Wolf, Markus "Algebraic System Specification and Development - Survey and Annotated Bibliography" Second Edition Compass Group Bremen 1997 Abstract ps Extract: Interactive Verification with COQ Extract:
  • Wiedijk, Freek (1998) Wiedijk, Freek "The Fifteen Provers of the World" Abstract
    Resources
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder