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.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Ciaffaglione, Alberto; Scagnetto, Ivan: Mechanizing type environments in weak HOAS (2015)
- Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
- Pientka, Brigitte; Cave, Andrew: Inductive Beluga: programming proofs (2015)
- Accattoli, Beniamino: Proof pearl: abella formalization of $\lambda $-calculus cube property (2012)
- Abel, Andreas; Pientka, Brigitte: Higher-order dynamic pattern unification for dependent types and records (2011)
- Felty, Amy; Pientka, Brigitte: Reasoning with higher-order abstract syntax and contexts: a comparison (2010)
- Pientka, Brigitte: Beluga: Programming with dependent types, contextual data, and contexts (2010)
- Pientka, Brigitte: Programming inductive proofs. A new approach based on contextual types (2010)
- Pientka, Brigitte; Dunfield, Joshua: Beluga: a framework for programming and reasoning with deductive systems (system description) (2010)