The following pages link to Delphin (Q33173):
Displaying 17 items.
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets (Q2890328) (← links)
- Extensible Datasort Refinements (Q2988653) (← links)
- Programs Using Syntax with First-Class Binders (Q2988654) (← links)
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (Q3007654) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance (Q3064169) (← links)
- A Coverage Checking Algorithm for LF (Q3559763) (← links)
- A Modular Type Reconstruction Algorithm (Q4617969) (← links)
- How to make ad hoc proof automation less ad hoc (Q5176973) (← links)
- Binders unbound (Q5176984) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- The calculus of dependent lambda eliminations (Q5372010) (← links)
- A logical framework combining model and proof theory (Q5400853) (← links)
- Theorem Proving in Higher Order Logics (Q5464654) (← links)
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description) (Q5747747) (← links)