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