A step-indexing approach to partial functions

DOI10.4204/EPTCS.114.4zbMATH Open1542.68216MaRDI QIDQ6587252FDOQ6587252

Authors: David Greve, Konrad Slind 

Publication date: 13 August 2024

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

Mathematics Subject Classification ID

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

Cites Work

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

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)