Isabelle
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Efficiently checking propositional refutations in HOL theorem provers
- Proof assistants: history, ideas and future
- Data compression for proof replay
- Graphical reasoning in compact closed categories for quantum computation
- Higher-order rewrite systems and their confluence
- A Skeptic's approach to combining HOL and Maple
- Winskel is (almost) right: Towards a mechanized semantics textbook
- ACL2
- AXIOM
- Labelled modal logics: Quantifiers
- Coq
- Experimenting with Isabelle in ZF set theory
- HOL-Boogie
- HYBRID
- Set theory for verification. I: From foundations to functions
- LEO-II
- Isabelle. A generic theorem prover
- Nitpick
- Ott
- Proviola
- Wooki
- woot-haskell
- wootjs
- Woot
- RelView
- Interactive theorem proving with temporal logic
- SACLIB
- TALP
- Theorema
- TkWinHOL
- TPS
- Towards the Mathematics Software Bus
- A first order logic of effects
- APS-1
- ML
- ALDOR
- Rapide
- Prosper
- Verified bytecode subroutines
- Bytecode verification by model checking
- Beluga
- COMBINE
- Isabelle/HOL
- MizarMode
- CoqJVM
- Isabelle/Isar
- IsaPlanner
- CAS/PI
- CASL
- VLISP
- OTTER
- HOL/SPIN
- ALISA
- Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings
- AVISPA
- The calculus of constructions as a framework for proof search with set variable instantiation
- Proof-search in type-theoretic languages: An introduction
- Natural deduction for non-classical logics
- RAISE
- Program development schemata as derived rules
- CCSL
- OMRS
- TCOZ
- MAYA
- More Church-Rosser proofs (in Isabelle/HOL)
- Isabelle/HOL. A proof assistant for higher-order logic
- PVS
- Proof planning for strategy development
- Haskell
- Paradox
- Evaluating general purpose automated theorem proving systems
- MathWebSearch
- A UTP approach for rTiMo
- CASPA_
- SPASS
- Maria
- ECCE
- Aligning concepts across proof assistant libraries
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings
- Why3
- Metis
- TLA
- CoSMed: a confidentiality-verified social media platform
- Toward compositional verification of interruptible OS kernels and device drivers
- Verified iptables firewall analysis and verification
- Hammer for Coq: automation for dependent type theory
- Formalization of the resolution calculus for first-order logic
- A deontic logic reasoning infrastructure
- Mechanized proofs of opacity: a comparison of two techniques
- Isar
- Omnibus
- distcc
- MetaPRL
- MoMM
- Mizar
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- A formally verified proof of the central limit theorem
- Kenzo
This page was built for software: Isabelle
