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