scientific article

Publication date: 5 June 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

functional programming theorem prover partial recursive functions

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items

Annotations in formal specifications and proofs, Inductive benchmarks for automated reasoning, Proof movie -- a proof with the Boyer-Moore prover, The reflective Milawa theorem prover is sound (down to the machine code that runs it), Invariants for the construction of a handshake register, An overview of the Tecton proof system, A formalization of powerlist algebra in ACL2, Foundations of a theorem prover for functional and mathematical uses, Mechanical verification on strategies, Proving Ramsey's theory by the cover set induction: A case and comparision study., The application of automated reasoning to questions in mathematics and logic, Verifying a distributed list system: A case history, Bounded delay for a free address, Convergence: integrating termination and abort-freedom, Theory extension in ACL2(r), A Ramsey theorem in Boyer-Moore logic, A mechanical proof of Segall's PIF algorithm, An integrated approach to high integrity software verification, Mathematical induction in Otter-lambda, SAD as a mathematical assistant -- how should we go from here to there?, New uses of linear arithmetic in automated theorem proving by induction, Middle-out reasoning for synthesis and induction, Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem, Using hints to increase the effectiveness of an automated reasoning program: Case studies, A temporal logic for real-time partial ordering with named transactions, A formalization of the Knuth-Bendix(-Huet) critical pair theorem, On extensibility of proof checkers, Getting saturated with induction, Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks, Techniques of computable set theory with applications to proof verification, Wait-free linearization with a mechanical proof, Rewriting with equivalence relations in ACL2, Wait-free concurrent memory management by Create and Read until Deletion (CaRuD), An ACL2 Tutorial, Using induction and rewriting to verify and complete parameterized specifications, Simulation Refinement for Concurrency Verification, On Shostak's decision procedure for combinations of theories, Circuits as streams in Coq: Verification of a sequential multiplier, On the comparison of HOL and Boyer-Moore for formal hardware verification, Incorporating quotation and evaluation into Church's type theory, A verification system for concurrent programs based on the Boyer-Moore prover, Machine checked proofs of the design of a fault-tolerant circuit, Simulation refinement for concurrency verification, Partial and nested recursive function definitions in higher-order logic, Verification by Parallelization of Parametric Code, A PVS Theory for Term Rewriting Systems, Herbrand's theorem and term induction, An ordinal measure based procedure for termination of functions, Automatic derivation of the irrationality of \(e\), Milestones from the Pure Lisp Theorem Prover to ACL2, Structuring and automating hardware proofs in a higher-order theorem- proving environment, N. G. de Bruijn's contribution to the formalization of mathematics, A Verified Runtime for a Verified Theorem Prover, Theories for mechanical proofs of imperative programs, Algebraic models of microprocessors architecture and organisation, Hybrid interactive theorem proving using nuprl and HOL, A verified common lisp implementation of Buchberger's algorithm in ACL2, Proof assistants: history, ideas and future, Operating system verification---an overview, Lazy techniques for fully expansive theorem proving, ACL2s: “The ACL2 Sedan”, A proof of the nonrestoring division algorithm and its implementation on an ALU, A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol, Specification and verification of concurrent programs through refinements

Uses Software

NQTHM