swMATH4624MaRDI QIDQ16795FDOQ16795
Author name not available (Why is that?)
Official website: http://www.cs.cornell.edu/jyh/metaprl/default.html
Cited In (36)
- Intuitionistic completeness of first-order logic
- Improving the Usability of HOL Through Controlled Automation Tactics
- Practical extraction of evidence terms from common-knowledge reasoning
- Building reliable, high-performance networks with the Nuprl proof development system
- Title not available (Why is that?)
- 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
- The strategy challenge in SMT solving
- Incorporating quotation and evaluation into Church's type theory
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Formalizing type operations using the ``image type constructor
- Title not available (Why is that?)
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
- Constructing categories and setoids of setoids in type theory
- distcc
- Omnibus
- ESC4
- Invariants for the FoCaL language
- KAT-ML
- FoCaL
- OpenAxiom
- HOL Light QE
- HOL2P
- Horus
- reFLect
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Bellerophon: tactical theorem proving for hybrid systems
- Practical reflection for sequent logics
This page was built for software: MetaPRL
