Building Decision Procedures in the Calculus of Inductive Constructions
From MaRDI portal
Publication:3608422
DOI10.1007/978-3-540-74915-8_26zbMath1179.68135arXiv0707.1266OpenAlexW1628824908MaRDI QIDQ3608422
Jean-Pierre Jouannaud, Frédéric Blanqui, Pierre-Yves Strub
Publication date: 5 March 2009
Published in: Computer Science Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0707.1266
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ High-Level Theories
Uses Software