MetaPRL
From MaRDI portal
Software:16795
No author found.
Related Items
Invariants for the FoCaL language ⋮ Formal compiler construction in a logical framework ⋮ Building reliable, high-performance networks with the Nuprl proof development system ⋮ Constructing categories and setoids of setoids in type theory ⋮ Innovations in computational type theory using Nuprl ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Intuitionistic completeness of first-order logic ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Improving the Usability of HOL Through Controlled Automation Tactics ⋮ Unnamed Item ⋮ Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics ⋮ Unnamed Item ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ HOL Light QE ⋮ The Strategy Challenge in SMT Solving ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Formalizing Type Operations Using the “Image” Type Constructor ⋮ Practical extraction of evidence terms from common-knowledge reasoning ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Theorem Proving in Higher Order Logics ⋮ KAT-ML: an interactive theorem prover for Kleene algebra with tests ⋮ Data compression for proof replay ⋮ Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection
This page was built for software: MetaPRL
