Kripke logical relations and PCF (Q1898483): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
| links / mardi / name | links / mardi / name | ||
Revision as of 13:46, 1 February 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Kripke logical relations and PCF |
scientific article |
Statements
Kripke logical relations and PCF (English)
0 references
11 May 1999
0 references
\textit{A. Jung} and \textit{J. Tiuryn} [Lect. Notes Comput. Sci. 664, 245-257 (1993; Zbl 0795.03021)] introduced ``Kripke logical relations'' to characterize \(\lambda\)-definability. Here, these relations are used to show that \textit{K. Sieber's} model of PCF [``New steps toward full abstraction for local variables'', in: ACM SIGLPLAN Workshop on State in Programming Languages, 88-100 (1993)], consisting of continuous functions that are invariant under certain (finitary) logical relations, is fully abstract at all types.
0 references
logic for computable functions
0 references
Kripke logical relations
0 references
full abstraction
0 references
