MetaPRL

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