A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
From MaRDI portal
Publication:2881085
DOI10.2168/LMCS-8(1:18)2012zbMath1238.68145arXiv1202.4905MaRDI QIDQ2881085
Enrico Tassi, Andrea Asperti, Claudio Sacerdoti Coen, Wilmer Ricciotti
Publication date: 3 April 2012
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1202.4905
type inference; calculus of inductive constructions; interactive theorem prover; \texttt{Matita}; refiner
Uses Software