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

DOI10.1017/S0960129500000384zbMath0802.68075MaRDI QIDQ4286532

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) Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items (6)

A stream calculus of bottomed sequences for real number computation ⋮ An abstract data type for real numbers ⋮ A stable programming language ⋮ Exploratory Functions on Nondeterministic Strategies, up to Lower Bisimilarity ⋮ Induction and recursion on the partial real line with applications to Real PCF ⋮ An abstract data type for real numbers

Cites Work

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

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