sign in
english version rss feed

inria-00497794, version 1

Coq Modulo Theory - Short Paper

Pierre-Yves Strub () 1, Qian Wang () 1

Logic In Computer Science (LICS 2010) (2010)

Abstract: Coq Modulo Theory (CoqMT) is an extension of the Coq proof assistant incorporating, in its computational mechanism, validity entailment for user-defined first-order equational theories. Such a mechanism strictly enriches the system (more terms are typable), eases the use of dependent types and provides more automation during the development of proofs. CoqMT improves over the Calculus of Congruent Inductive Constructions by getting rid of various restrictions and simplifying the type-checking algorithm and the integration of first-order decision procedures.

  • 1:  FORMES (LIAMA)
  • INRIA – Tsinghua University / Beijing – LIAMA
  • Domain : Computer Science/Logic in Computer Science
 
  • inria-00497794, version 1
  • oai:hal.inria.fr:inria-00497794
  • From: 
  • Submitted on: Monday, 5 July 2010 23:51:58
  • Updated on: Tuesday, 6 July 2010 09:37:34
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...