Isabelle. A generic theorem prover
From MaRDI portal
Publication:1331625
DOI10.1007/BFb0030541zbMath0825.68059MaRDI QIDQ1331625
Publication date: 22 August 1994
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
68-02: Research exposition (monographs, survey articles) pertaining to computer science
Related Items
Verified lightweight bytecode verification, Hoare logic for Java in Isabelle/HOL, Mechanizing Nonstandard Real Analysis, Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology, The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf, High-Level Theories, Combining Isabelle and QEPCAD-B in the Prover’s Palette, A higher-order interpretation of deductive tableau, Balancing the load. Leveraging a semantics stack for systems verification, Ordinal arithmetic: Algorithms and mechanization, TPS: A hybrid automatic-interactive system for developing proofs, A proof-centric approach to mathematical assistants, Computer supported mathematics with \(\Omega\)MEGA, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, The seven virtues of simple type theory, Efficiently checking propositional refutations in HOL theorem provers, Data compression for proof replay, Performance analysis and functional verification of the stop-and-wait protocol in HOL, Graphical reasoning in compact closed categories for quantum computation, Higher-order rewrite systems and their confluence, Towards the Mathematics Software Bus, A first order logic of effects, Reuse of proofs in software verification, The calculus of constructions as a framework for proof search with set variable instantiation, Proof-search in type-theoretic languages: An introduction, Program development schemata as derived rules, Evaluating general purpose automated theorem proving systems, CASL: the Common Algebraic Specification Language., Structuring metatheory on inductive definitions, Nominal logic, a first order theory of names and binding, Decidability of bounded higher-order unification, An approach to automatic deductive synthesis of functional programs, On the mechanization of the proof of Hessenberg's theorem in coherent logic, Rewriting conversions implemented with continuations, Admissibility of structural rules for contraction-free systems of intuitionistic logic, Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model, Translating a Dependently-Typed Logic to First-Order Logic, A Declarative Language for the Coq Proof Assistant, Modelling Attacker’s Knowledge for Cascade Cryptographic Protocols, Automating Algebraic Specifications of Non-freely Generated Data Types, The Isabelle Framework, LCF-Style Propositional Simplification with BDDs and SAT Solvers, Lightweight Separation, Real Number Calculations and Theorem Proving, 1998 European Summer Meeting of the Association for Symbolic Logic
Uses Software
