Beluga

Our main interest in this project is to investigate programming and reasoning with data structures that provide support for binders. Many object languages include binding constructs, and it is striking that functional languages still lack direct support for binders and common tricky operations such as renaming, capture-avoiding substitution, and fresh name generation. We advocate the use of higher-order abstract syntax (HOAS) where we represent binders in the object language with binders in the meta-language. One of the key benefits is that we not only get support for renaming and fresh name generation, but also for capture-avoiding substitution. While HOAS encodings have played an important role in mechanizing the meta-theory of programming languages, it has been difficult to incorporate HOAS encodings directly into functional programming.


References in zbMATH (referenced in 25 articles , 1 standard article )

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

1 2 next

  1. Abel, Andreas; Allais, Guillaume; Hameer, Aliya; Pientka, Brigitte; Momigliano, Alberto; Schäfer, Steven; Stark, Kathrin: POPLMark reloaded: mechanizing proofs by logical relations (2019)
  2. Mahmoud, Mohamed Yousri; Felty, Amy P.: Formalization of metatheory of the quipper quantum programming language in a linear logic (2019)
  3. Miller, Dale: Mechanized metatheory Revisited (2019)
  4. Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David: A case study in programming coinductive proofs: Howe’s method (2019)
  5. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  6. Rabe, Florian: A modular type reconstruction algorithm (2018)
  7. Dunfield, Joshua: Extensible datasort refinements (2017)
  8. Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: \textscLincx: a linear logical framework with first-class contexts (2017)
  9. Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: (\mathsfLLF_\mathcalP): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
  10. Kaiser, Jonas; Pientka, Brigitte; Smolka, Gert: Relating system F and (\lambda2): a case study in Coq, Abella and Beluga (2017)
  11. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
  12. Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
  13. Ciaffaglione, Alberto; Scagnetto, Ivan: Mechanizing type environments in weak HOAS (2015)
  14. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  15. Pientka, Brigitte; Cave, Andrew: Inductive Beluga: programming proofs (2015)
  16. Ronan Saillard: Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice (2015) not zbMATH
  17. Steen, Alexander; Benzmüller, Christoph: There is no best (\beta)-normalization strategy for higher-order reasoners (2015)
  18. Savary-Belanger, Olivier; Monnier, Stefan; Pientka, Brigitte: Programming type-safe transformations using higher-order abstract syntax (2013)
  19. Accattoli, Beniamino: Proof pearl: Abella formalization of (\lambda)-calculus cube property (2012)
  20. Abel, Andreas; Pientka, Brigitte: Higher-order dynamic pattern unification for dependent types and records (2011)

1 2 next