A step-indexing approach to partial functions

DOI10.4204/EPTCS.114.4MaRDI QIDQ6587252zbMATH OpenFDO

Authors David Greve, Konrad Slind

Publication date 13 August 2024

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Recursive functions and relations, subrecursive hierarchies (03D20)

Recommendations

• Partial functions in ACL2
• Partial functions in a total setting
• Partial and nested recursive function definitions in higher-order logic
• Partial Recursive Functions in Higher-Order Logic
• Partiality and recursion in interactive theorem provers -- an overview

Cites work

• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Notions of computation and monads
• Partial and nested recursive function definitions in higher-order logic
• Partial functions in ACL2
• Structured theory development for a mechanized logic

This page was built for publication: A step-indexing approach to partial functions

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