A universality theorem for PCF with recursive types, parallel-or and ∃

DOI10.1017/S0960129500000384MaRDI QIDQ4286532zbMATH OpenFDO

Authors Thomas Streicher

Publication date 11 December 1994

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

PCFtyped \(\lambda\)-calculusrecursive typesuniversal programming languageminimal fixpoint operator

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 1968604
• Full abstraction and the Context Lemma (preliminary report)
• scientific article; zbMATH DE number 16188
• scientific article; zbMATH DE number 1523049
• Full abstraction, totality and PCF

Cites work

• Effectively given domains
• Expressibility of functionals in D. Scott's LCF language
• LCF considered as a programming language

Cited in

(6)

• An abstract data type for real numbers
• A stable programming language
• An abstract data type for real numbers
• Exploratory functions on nondeterministic strategies, up to lower bisimilarity
• Induction and recursion on the partial real line with applications to Real PCF
• A stream calculus of bottomed sequences for real number computation

This page was built for publication: A universality theorem for PCF with recursive types, parallel-or and ∃

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4286532)