Partial functions in ACL2

DOI10.1023/B:JARS.0000009505.07087.34zbMath1060.68109WikidataQ61863664 ScholiaQ61863664MaRDI QIDQ1425160

Panagiotis Manolios, J. Strother Moore

Publication date: 15 March 2004

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

partial functionsACL2

Mathematics Subject Classification ID

Related Items (12)

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Function extraction ⋮ Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ A mechanical analysis of program verification strategies ⋮ An ACL2 Tutorial ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Transforming Programs into Recursive Functions ⋮ Adapting functional programs to higher order logic ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• ACL2

This page was built for publication: Partial functions in ACL2