The following pages link to MetaPRL (Q16795):
Displaying 26 items.
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Practical extraction of evidence terms from common-knowledge reasoning (Q530856) (← links)
- Formal compiler construction in a logical framework (Q853741) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- Data compression for proof replay (Q1040776) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- HOL Light QE (Q1791161) (← links)
- Invariants for the FoCaL language (Q2379680) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- (Q2754047) (← links)
- Practical reflection for sequent logics (Q2871862) (← links)
- Constructing categories and setoids of setoids in type theory (Q2921123) (← links)
- Improving the Usability of HOL Through Controlled Automation Tactics (Q3523173) (← links)
- Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics (Q3535610) (← links)
- KAT-ML: an interactive theorem prover for Kleene algebra with tests (Q3647254) (← links)
- (Q4447229) (← links)
- (Q4484346) (← links)
- Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
- (Q4783332) (← links)
- Building reliable, high-performance networks with the Nuprl proof development system (Q4819652) (← links)
- The Strategy Challenge in SMT Solving (Q4913859) (← links)
- Formalizing Type Operations Using the “Image” Type Constructor (Q4917993) (← links)
- (Q5094128) (← links)
- Theorem Proving in Higher Order Logics (Q5464643) (← links)
- Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection (Q5501464) (← links)
