Delphin
From MaRDI portal
Software:33173
No author found.
Related Items (17)
Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ A two-level logic approach to reasoning about computations ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ The calculus of dependent lambda eliminations ⋮ A Modular Type Reconstruction Algorithm ⋮ Extensible Datasort Refinements ⋮ Programs Using Syntax with First-Class Binders ⋮ A logical framework combining model and proof theory ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ A formalized general theory of syntax with bindings: extended version ⋮ A Coverage Checking Algorithm for LF ⋮ How to make ad hoc proof automation less ad hoc ⋮ Binders unbound ⋮ Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) ⋮ Programming Inductive Proofs ⋮ Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance ⋮ Theorem Proving in Higher Order Logics
This page was built for software: Delphin
