Delphin
From MaRDI portal
swMATH21365MaRDI QIDQ33173FDOQ33173
Author name not available (Why is that?)
Official website: https://www.itu.dk/~carsten/papers/delphin.pdf
Cited In (33)
- 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
- The calculus of dependent lambda eliminations
- HYBRID
- Beluga
- Twelf
- Abella
- Cayenne
- LNgen
- Rtac
- RepLib
- VeriML
- Mtac: a monad for typed tactic programming in Coq
- FreshML
- A coverage checking algorithm for LF
- Programming inductive proofs. A new approach based on contextual types
- Stardust
- LLFp
- Forsythe
- FreshOCaml
- HNT
- Unbound
- 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
- Programs using syntax with first-class binders
This page was built for software: Delphin
