Substitution: A Formal Methods Case Study Using Monads and Transformations

By F. Bellegarde, J. Hook. 1994

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Heterogeneous substitution systems revisited (2016, neutral): “Any opinions, ﬁndings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reﬂect the views of the National Science Foundation.”
Monadic Presentations of Lambda Terms Using Generalized Inductive Types (1999, result): “We find a partial answer in the work of Bellegarde and Hook [ BH94 ] who take the view that lambda terms should be represented by an operator Lam ∈ Set → Set, where Set denotes the universe of sets, such that Lam(X) is the set of λ-terms with variables in X. This corresponds to the presentation of t”
Substitution in Non-wellfounded Syntax with Variable Binding (2003, background): “The rank 2 inductive constructor representation of the untyped lambda calculus syntax in the de Bruijn version in either a functional language or a typed lambda calculus is implicit in Bellegarde and Hook [9] and appears explicated in Altenkirch and Reus [7] and Bird and Paterson [12](remarkably, Al”
Map fusion for nested datatypes in intensional type theory (2011, background): “The basic example where variable binding is represented through a nested datatype is a typeful de Bruijn representation of untyped lambda calculus, following ideas of [4, 5, 6].”