Codifying guarded definitions with recursive schemes

DOI10.1007/3-540-60579-7_3zbMath1530.03054OpenAlexW1980786790MaRDI QIDQ6083895

Unnamed Author

Publication date: 8 December 2023

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

Full work available at URL: https://doi.org/10.1007/3-540-60579-7_3

zbMATH Keywords

proof systemcase analysisreduction rulerecursive calltyping rule

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items

Turing-Completeness Totally Free, Quotients by Idempotent Functions in Cedille, Unnamed Item, Friends with Benefits, Undecidability of equality for codata types

Cites Work

• A co-induction principle for recursively defined domains
• Introduction to generalized type systems
• Unnamed Item
• Unnamed Item