Partial functions in ACL2
From MaRDI portal
Publication:1425160
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)
Related Items
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
