Delphin
From MaRDI portal
Cited in
(33)- 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
- Towards logical frameworks in the heterogeneous tool set Hets
- A formalized general theory of syntax with bindings: extended version
- A Modular Type Reconstruction Algorithm
- Refinement types for logical frameworks and their interpretation as proof irrelevance
- Theorem Proving in Higher Order Logics
- HYBRID
- Beluga
- Twelf
- Abella
- Cayenne
- LNgen
- Rtac
- RepLib
- VeriML
- Stardust
- LLFp
- Forsythe
- FreshOCaml
- HNT
- Unbound
- The calculus of dependent lambda eliminations
- FreshML
- Programming inductive proofs. A new approach based on contextual types
- Mtac: a monad for typed tactic programming in Coq
- A coverage checking algorithm for LF
- Binders unbound
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Extensible Datasort Refinements
- A two-level logic approach to reasoning about computations
- How to make ad hoc proof automation less ad hoc
This page was built for software: Delphin
