Closure calculus is simpler than pure lambda-calculus as it does not mention free variables or index manipulation, variable renaming, implicit substitution, or any other meta-theory. Further, all programs, even recursive ones, can be expressed as normal forms. Third, there are reduction-preserving translations to calculi built from combinations of operators, in the style of combinatory logic. These improvements are achieved without sacrificing three fundamental properties of lambda-calculus, being a confluent rewriting system, supporting the Turing computable numerical functions, and supporting simple typing.
Mon 14 Jan
|11:00 - 11:05|
|11:05 - 12:00|
Christian HumerOracle Labs, SwitzerlandFile Attached
|12:00 - 12:30|
Barry JayUniversity of Technology SydneyDOI