Title :
Full abstraction and universality via realisability
Author :
Marz, Michael ; Rohr, Alexander ; Streicher, Thomas
Author_Institution :
Fachbereich Math., Tech. Univ. Darmstadt, Germany
Abstract :
We construct fully abstract realisability models of PCF. In particular, we prove a variant of the Longley-Phoa Conjecture by showing that the realisability model over an untyped λ-calculus with arithmetic is fully abstract for PCF. Further we consider the extension of our results to a general sequential functional programming language SFPL giving rise to universal realisability models for SFPL
Keywords :
lambda calculus; λ-calculus; PCF; abstract realisability; sequential functional programming language; untyped λcalculus; Arithmetic; Calculus; Computational modeling; Computer languages; Context modeling; Equations; Functional programming; Principal component analysis;
Conference_Titel :
Logic in Computer Science, 1999. Proceedings. 14th Symposium on
Conference_Location :
Trento
Print_ISBN :
0-7695-0158-3
DOI :
10.1109/LICS.1999.782612