Kripke logical relations and PCF (Q1898483): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W1965557765 / rank | |||
Normal rank | |||
Revision as of 21:19, 19 March 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
