posted on 2013-06-11, 10:45authored byPaula Severi, Fer-Jan de Vries
In 1970 Friedman proved completeness of beta eta conversion in the simply-typed lambda calculus for the set-theoretical model. Recently Krishnaswami and Benton have captured the essence of Hudak’s reactive programs in an extension of simply typed lambda calculus with causal streams and a temporal modality and provided this typed lambda calculus for reactive programs with a sound ultrametric semantics.
We show that beta eta conversion in the typed lambda calculus of reactive programs is complete for the ultrametric model.
History
Citation
Lecture Notes in Computer Science, 2013, 7941, pp. 221-235
Author affiliation
/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science
Source
11th International Conference on Typed Lambda Calculi and Applications (TLCA), Eindhoven