Kripke logical relations and PCF (Q1898483): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Created claim: Wikidata QID (P12): Q56092885, #quickstatements; #temporary_batch_1706897434465 |
||
| Property / Wikidata QID | |||
| Property / Wikidata QID: Q56092885 / rank | |||
Normal rank | |||
Revision as of 20:46, 2 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
