Induction and recursion on the partial real line with applications to Real PCF

DOI10.1016/S0304-3975(98)00099-1zbMath0912.68123OpenAlexW2157014216MaRDI QIDQ1274810

Thomas Streicher, Martín Hötzel Escardó

Publication date: 12 January 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(98)00099-1

zbMATH Keywords

universalityinductiondomain theorycoinductionexact real number computationreal PCF

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items

Semantics of a sequential language for exact real-number computation, A Real Elementary Approach to the Master Recurrence and Generalizations, Semi-decidability of May, Must and Probabilistic Testing in a Higher-type Setting, Computable de Finetti measures, An extension of the dual complexity space and an application to computer science, Integration in Real PCF

Cites Work

• \(\mathbb{T}^\omega\) as a universal domain
• Effectively given domains
• Computability concepts for programming language semantics
• LCF considered as a programming language
• A domain-theoretic approach to computability on the real line
• Properly injective spaces and function spaces
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• PCF extended with real numbers
• Edinburgh LCF. A mechanized logic of computation
• A coinduction principle for recursive data types based on bisimulation
• Algebraic specification of data types: A synthetic approach
• The Category-Theoretic Solution of Recursive Domain Equations
• A universality theorem for PCF with recursive types, parallel-or and ∃
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item