A modest model of records, inheritance, and bounded quantification

DOI10.1016/0890-5401(90)90062-MzbMath0711.68072MaRDI QIDQ922718

Kim B. Bruce

Publication date: 1990

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

zbMATH Keywords

model-theoretic semanticssecond-order lambda calculussemantics of inheritance

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items

An operational semantics for TOOPLE: A statically-typed object-oriented programming language ⋮ Unnamed Item ⋮ Coherence of subsumption, minimum typing and type-checking in F ≤ ⋮ Labelled reductions, runtime errors, and operational subsumption ⋮ Termination of system \(F\)-bounded: A complete proof ⋮ A lambda-calculus for dynamic binding ⋮ Subtyping + extensionality: Confluence of βηtop reduction in F≤ ⋮ An extension of system F with subtyping ⋮ An imperative object calculus ⋮ Higher-order subtyping ⋮ The equivalence of two semantic definitions for inheritance in object-oriented languages ⋮ Typed operational semantics for higher-order subtyping. ⋮ Toward a semantics for the QUEST language ⋮ Divergence of \(F_{\leq}\) type checking ⋮ Logical equivalence for subtyping object and recursive types ⋮ Unification in an extensional lambda calculus with ordered function sorts and constant overloading ⋮ Game Semantics for Bounded Polymorphism ⋮ Another definition of order-sorted algebra ⋮ Subtyping in Logical Form ⋮ Basic theory of \(F\)-bounded quantification. ⋮ A sequent calculus for subtyping polymorphic types ⋮ A paradigmatic object-oriented programming language: Design, static typing and semantics ⋮ Simple type-theoretic foundations for object-oriented programming ⋮ CPO-models for second order lambda calculus with recursive types and subtyping ⋮ Polymorphic lambda calculus and subtyping.

Uses Software

• Smalltalk
• Eiffel
• Simula 67

Cites Work

• Extensional models for polymorphism
• The semantics of second-order lambda calculus
• Functorial polymorphism
• Polymorphic type inference and containment
• A small complete category
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• Recursion over realizability structures
• ABOUT MODEST SETS
• The Discrete Objects in the Effective Topos
• Categorical semantics for higher order polymorphic lambda calculus
• Constructive natural deduction and its ‘ω-set’ interpretation
• 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