Delphin

Delphin: Functional programming with deductive systems. We present the design and implementation of the strict and pure functional programming language Delphin. Its novel and distinctive features include a two-level design that distinguishes cleanly between the tasks of representing data and programming with data. One level is the logical framework LF [5], serving as Delphin’s data representation language. The other level is T+! [15], a type theory designed to support programming using pattern matching and recursion. The main contribution of this work is therefore Delphin, in which one can program with higher-order, dependently-typed data structures such as proofs and typing derivations in a natural and intuitive way


References in zbMATH (referenced in 18 articles )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  2. Rabe, Florian: A modular type reconstruction algorithm (2018)
  3. Dunfield, Joshua: Extensible datasort refinements (2017)
  4. Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
  5. Stump, Aaron: The calculus of dependent lambda eliminations (2017)
  6. Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor: Mtac: a monad for typed tactic programming in Coq (2015)
  7. Rabe, Florian: A logical framework combining model and proof theory (2013)
  8. Codescu, Mihai; Horozal, Fulya; Kohlhase, Michael; Mossakowski, Till; Rabe, Florian; Sojakova, Kristina: Towards logical frameworks in the heterogeneous tool set Hets (2012)
  9. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  10. Abel, Andreas; Pientka, Brigitte: Higher-order dynamic pattern unification for dependent types and records (2011)
  11. Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek: How to make ad hoc proof automation less ad hoc (2011)
  12. Weirich, Stephanie; Yorgey, Brent A.; Sheard, Tim: Binders unbound (2011)
  13. Lovas, William; Pfenning, Frank: Refinement types for logical frameworks and their interpretation as proof irrelevance (2010)
  14. Pientka, Brigitte: Programming inductive proofs. A new approach based on contextual types (2010)
  15. Pientka, Brigitte; Dunfield, Joshua: Beluga: a framework for programming and reasoning with deductive systems (system description) (2010)
  16. Poswolsky, Adam; Schürmann, Carsten: System description: Delphin -- a functional programming language for deductive systems (2009) ioport
  17. Anderson, Penny; Pfenning, Frank: Verifying uniqueness in a logical framework (2004)
  18. Schürmann, Carsten; Pfenning, Frank: A coverage checking algorithm for LF (2003)