Paper Info
Title
Linearity and recursion in a typed Lambda-calculus
Abstract
We show that the full PCF language can be encoded in L_rec, a syntactically linear λ-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for L_rec, exploiting its linearity.
Year
DOI
Venue
2011
10.1145/2003476.2003500
PPDP
Keywords
Field
DocType
call-by-value evaluation strategy,syntactic linearity,implementation technique,unbounded recursor,full pcf language,lambda calculus,typed lambda calculus,recursion
Discrete mathematics,Typed lambda calculus,Simply typed lambda calculus,Lambda cube,Computer science,Fixed-point combinator,System F,Algorithm,Theoretical computer science,Church encoding,Pure type system,Curry–Howard correspondence
Conference
Citations 
PageRank 
References 
2
0.37
38
Authors
4
Name
Order
Citations
PageRank
Sandra Alves1388.47
Maribel Fernández231523.44
Mário Florido320.71
Ian Mackie4889.58