H ? « »

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


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

  • (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
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder