Lexicographic Path Induction

DOI10.1007/978-3-642-02273-9_21MaRDI QIDQ3637202zbMATH OpenOpenAlexFDO

Authors Jeffrey Sarnat, Carsten Schürmann

Publication date 7 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-02273-9_21

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Theory of programming languages (68N15)

Recommendations

• scientific article; zbMATH DE number 4014064
• Inductive beluga: programming proofs
• Well-founded Relations in Type Theory
• Inductive families
• Induction = I-axiomatization + first-order consistency.

Cites work

• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Cut-elimination for a logic with definitions and induction
• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 3572133 (Why is no real title available?)
• scientific article; zbMATH DE number 1302675 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3365218 (Why is no real title available?)
• Proof-theoretic analysis of termination proofs
• Types for Proofs and Programs

This page was built for publication: Lexicographic Path Induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3637202)