MetaPRL

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
• 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
• Invariants for the FoCaL language
• 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