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
- Higher-order dynamic pattern unification for dependent types and records
- Programs Using Syntax with First-Class Binders
- Mtac: A monad for typed tactic programming in Coq
- 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
- A coverage checking algorithm for LF
- Programming inductive proofs. A new approach based on contextual types
- 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
