Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I

DOI10.1016/j.entcs.2007.02.050zbMath1277.68101OpenAlexW2070114636MaRDI QIDQ2866803

Claudio Sacerdoti Coen

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.02.050

zbMATH Keywords

abstract machineconversioncalculus of inductive constructionreduction strategy

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (1)

A compact kernel for the calculus of inductive constructions

Uses Software

• Coq
• Automath

Cites Work

• Type checking with universes
• The duality of computation
• Mathematical Knowledge Management
• Unnamed Item
• Unnamed Item

This page was built for publication: Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I