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