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 15 articles , 1 standard article )

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

  1. Dunfield, Joshua: Extensible datasort refinements (2017)
  2. Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: Lincx: a linear logical framework with first-class contexts (2017)
  3. Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: $\mathsfLLF_\CalP$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
  4. Wang, Yuting; Nadathur, Gopalan: A higher-order abstract syntax approach to verified transformations on functional programs (2016)
  5. Ciaffaglione, Alberto; Scagnetto, Ivan: Mechanizing type environments in weak HOAS (2015)
  6. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  7. Pientka, Brigitte; Cave, Andrew: Inductive Beluga: programming proofs (2015)
  8. Steen, Alexander; Benzm├╝ller, Christoph: There is no best $\beta $-normalization strategy for higher-order reasoners (2015)
  9. Accattoli, Beniamino: Proof pearl: abella formalization of $\lambda $-calculus cube property (2012)
  10. Abel, Andreas; Pientka, Brigitte: Higher-order dynamic pattern unification for dependent types and records (2011)
  11. Weirich, Stephanie; Yorgey, Brent A.; Sheard, Tim: Binders unbound (2011)
  12. Felty, Amy; Pientka, Brigitte: Reasoning with higher-order abstract syntax and contexts: a comparison (2010)
  13. Pientka, Brigitte: Beluga: Programming with dependent types, contextual data, and contexts (2010) ioport
  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)