The following pages link to Isabelle (Q13212):
Displaying 50 items.
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (Q865658) (← links)
- Verification of FPGA layout generators in higher-order logic (Q877830) (← 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)
- Using formal reasoning on a model of tasks for FreeRTOS (Q903515) (← links)
- A mechanized proof of the basic perturbation lemma (Q928666) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Generating certified code from formal proofs: a case study in homological algebra (Q968307) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Graphical reasoning in compact closed categories for quantum computation (Q1044227) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- A Skeptic's approach to combining HOL and Maple (Q1272607) (← links)
- Winskel is (almost) right: Towards a mechanized semantics textbook (Q1272764) (← links)
- Labelled modal logics: Quantifiers (Q1289100) (← links)
- Experimenting with Isabelle in ZF set theory (Q1312157) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- Isabelle. A generic theorem prover (Q1331625) (← links)
- Interactive theorem proving with temporal logic (Q1355780) (← links)
- Towards the Mathematics Software Bus (Q1389634) (← links)
- A first order logic of effects (Q1390955) (← links)
- Verified bytecode subroutines (Q1405993) (← links)
- Bytecode verification by model checking (Q1405996) (← links)
- Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings (Q1567498) (← 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)
- Natural deduction for non-classical logics (Q1577342) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- More Church-Rosser proofs (in Isabelle/HOL) (Q1595924) (← links)
- Isabelle/HOL. A proof assistant for higher-order logic (Q1600086) (← links)
- Proof planning for strategy development (Q1601860) (← links)
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- A UTP approach for rTiMo (Q1624596) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings (Q1653699) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- Verified iptables firewall analysis and verification (Q1663231) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A deontic logic reasoning infrastructure (Q1670720) (← links)
- Mechanized proofs of opacity: a comparison of two techniques (Q1673658) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation (Q1687724) (← links)
- FoCaLiZe and Dedukti to the rescue for proof interoperability (Q1687726) (← links)
- A formally verified proof of the central limit theorem (Q1694568) (← links)
- Fermat, Euler, Wilson -- three case studies in number theory (Q1707601) (← links)
- Towards verification of cyber-physical systems with UTP and Isabelle/HOL (Q1708708) (← links)
