A New Elimination Rule for the Calculus of Inductive Constructions

DOI10.1007/978-3-642-02444-3_3zbMath1246.68085OpenAlexW1571309311MaRDI QIDQ3638245

Jorge Luis Sacchini, Hugo Herbelin, Pierre Corbineau, Benjamin Grégoire, Bruno Barras

Publication date: 2 July 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-642-02444-3_3

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (1)

Eliminating dependent pattern matching without K

Uses Software

• Coq
• Epigram

Cites Work

• Unnamed Item
• A Coverage Checking Algorithm for LF
• Subset Coercions in Coq
• The view from the left
• Advanced Functional Programming
• Eliminating Dependent Pattern Matching

This page was built for publication: A New Elimination Rule for the Calculus of Inductive Constructions