Cited in
(36)- Intuitionistic completeness of first-order logic
- Practical extraction of evidence terms from common-knowledge reasoning
- Improving the Usability of HOL Through Controlled Automation Tactics
- Building reliable, high-performance networks with the Nuprl proof development system
- scientific article; zbMATH DE number 1927428 (Why is no real title available?)
- Faster and more complete extended static checking for the Java modeling language
- Theorem Proving in Higher Order Logics
- Formal compiler construction in a logical framework
- Incorporating quotation and evaluation into Church's type theory
- The strategy challenge in SMT solving
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Formalizing type operations using the ``image type constructor
- scientific article; zbMATH DE number 1670747 (Why is no real title available?)
- distcc
- Omnibus
- ESC4
- KAT-ML
- FoCaL
- OpenAxiom
- HOL2P
- Horus
- reFLect
- HOL Light QE
- Constructing categories and setoids of setoids in type theory
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
- Invariants for the FoCaL language
- HOL Light QE
- Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
- Validating Brouwer's continuity principle for numbers using named exceptions
- Innovations in computational type theory using Nuprl
- Data compression for proof replay
- scientific article; zbMATH DE number 2043526 (Why is no real title available?)
- scientific article; zbMATH DE number 7566056 (Why is no real title available?)
- scientific article; zbMATH DE number 1841844 (Why is no real title available?)
- Bellerophon: tactical theorem proving for hybrid systems
- Practical reflection for sequent logics
This page was built for software: MetaPRL
