A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

DOI10.2168/LMCS-8(1:18)2012zbMath1238.68145arXiv1202.4905MaRDI QIDQ2881085

Wilmer Ricciotti, Andrea Asperti, Enrico Tassi, Claudio Sacerdoti Coen

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

zbMATH Keywords

type inferencecalculus of inductive constructionsinteractive theorem prover\texttt{Matita}refiner

Mathematics Subject Classification ID

Related Items (5)

I Got Plenty o’ Nuttin’ ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Unnamed Item ⋮ A formalization of multi-tape Turing machines ⋮ Implementing type theory in higher order constraint logic programming

Uses Software

• Coq
• Matita
• Automath
• Agda

This page was built for publication: A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions