Recursion over realizability structures

DOI10.1016/0890-5401(91)90074-CzbMath0760.03012MaRDI QIDQ1173956

Roberto M. Amadio

Publication date: 25 June 1992

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

inductive typesCartesian closed categorycomplete partial ordersScott domainfixed-point operatorcontractive operatorsGirard's system \(F\)higher-order domain equationshigher-order lambda-calculusmodelling of recursive definitions of programs and typesrealizability modelrealizability structuresrecursion on types

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Applications of computability and recursion theory (03D80) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items

The category-theoretic solution of recursive metric-space equations, The equivalence of two semantic definitions for inheritance in object-oriented languages, An exper model for Quest, A relational realizability model for higher-order stateful ADTs, A modest model of records, inheritance, and bounded quantification, Inheritance as implicit coercion, Recursive types for Fun, Toward a semantics for the QUEST language, Partiality, State and Dependent Types, Categorical models of polymorphism, Logical equivalence for subtyping object and recursive types, Realisability semantics of parametric polymorphism, general references and recursive types, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, On functions preserving levels of approximation: A refined model construction for various lambda calculi, Subtyping in Logical Form, Basic theory of \(F\)-bounded quantification., Type destructors, A paradigmatic object-oriented programming language: Design, static typing and semantics, Baby Modula-3 and a theory of objects, Combining type disciplines

Cites Work

• 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
• Extensional models for polymorphism
• Fundamental properties of infinite trees
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• Partial morphisms in categories of effective objects
• Polymorphic type inference and containment
• A small complete category
• Metric interpretations of infinite trees and semantics of non deterministic recursive programs
• Recursive types for Fun
• Constructivism in mathematics. An introduction. Volume II
• Elementary induction on abstract structures
• Fixed-point constructions in order-enriched categories
• Domain theoretic models of polymorphism
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• An ideal model for recursive polymorphic types
• The Category-Theoretic Solution of Recursive Domain Equations
• Data Types as Lattices
• On the interpretation of intuitionistic number theory