Pages that link to "Item:Q1331625"
From MaRDI portal
The following pages link to Isabelle. A generic theorem prover (Q1331625):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A scalable module system (Q391632) (← links)
- Automated type-based analysis of injective agreement in the presence of compromised principals (Q492914) (← links)
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
- Reasoning about conditional probabilities in a higher-order-logic theorem prover (Q545151) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Automating Event-B invariant proofs by rippling and proof patching (Q667526) (← links)
- The world's shortest correct exact real arithmetic program? (Q714620) (← links)
- Implementing type systems for the IDE with Xsemantics (Q739624) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- Balancing the load. Leveraging a semantics stack for systems verification (Q835780) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols (Q880981) (← links)
- A complete axiom system for propositional projection temporal logic with cylinder computation model (Q896162) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Performance analysis and functional verification of the stop-and-wait protocol in HOL (Q1040781) (← links)
- Graphical reasoning in compact closed categories for quantum computation (Q1044227) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- Towards the Mathematics Software Bus (Q1389634) (← links)
- A first order logic of effects (Q1390955) (← links)
- Reuse of proofs in software verification (Q1419888) (← links)
- The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- A UTP approach for rTiMo (Q1624596) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- Verifying OpenJDK's sort method for generic collections (Q1725846) (← links)
- A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (Q1798665) (← links)
- CASL: the Common Algebraic Specification Language. (Q1853453) (← links)
- Structuring metatheory on inductive definitions (Q1854368) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- Twenty years of rewriting logic (Q1931904) (← links)
- A process calculus BigrTiMo of mobile systems and its formal semantics (Q2026376) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Logic-independent proof search in logical frameworks (short paper) (Q2096460) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
