MetaPRL
From MaRDI portal
Software:16795
swMATH4624MaRDI QIDQ16795FDOQ16795
Author name not available (Why is that?)
Cited In (26)
- 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
- Incorporating quotation and evaluation into Church's type theory
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection
- 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
- Invariants for the FoCaL language
- HOL Light QE
- 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?)
- The Strategy Challenge in SMT Solving
- Bellerophon: tactical theorem proving for hybrid systems
- Formalizing Type Operations Using the “Image” Type Constructor
- Practical reflection for sequent logics
This page was built for software: MetaPRL
