Inheritance as implicit coercion

DOI10.1016/0890-5401(91)90055-7zbMath0799.68129OpenAlexW2144778998MaRDI QIDQ1175335

Carl A. Gunter, Val Breazu-Tannen, Thierry Coquand, Andrej Scedrov

Publication date: 25 June 1992

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

Full work available at URL: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1790&context=cis_reports

zbMATH Keywords

type structure\(\lambda\)-calculusprogram and recursion schemes

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items (27)

Explicit effect subtyping ⋮ A syntax for linear logic ⋮ Session types and subtyping for orchestrated interactions ⋮ A model for syntactic control of interference ⋮ Higher-order subtyping and its decidability ⋮ Labelled reductions, runtime errors, and operational subsumption ⋮ Integration of parametric and ``ad hoc second order polymorphism in a calculus with subtyping ⋮ A lambda-calculus for dynamic binding ⋮ The coherence of languages with intersection types ⋮ Higher-order subtyping ⋮ Coercions in a polymorphic type system ⋮ Operational interpretations of an extension of F_ω with control operators ⋮ Structural subtyping for inductive types with functorial equality rules ⋮ Logical equivalence for subtyping object and recursive types ⋮ Type-based hot swapping of running modules ⋮ Unnamed Item ⋮ Subtyping dependent types ⋮ Coherence of subsumption for monadic types ⋮ COCHIS: Stable and coherent implicits ⋮ Refinement Types as Proof Irrelevance ⋮ Unnamed Item ⋮ Type-directed specialization of polymorphism. ⋮ A Parametric Calculus for Mobile Open Code ⋮ A paradigmatic object-oriented programming language: Design, static typing and semantics ⋮ CPO-models for second order lambda calculus with recursive types and subtyping ⋮ Polymorphic lambda calculus and subtyping. ⋮ Open and closed scopes for constrained genericity

Uses Software

• Smalltalk

Cites Work

• Linear logic
• Extensional models for polymorphism
• A note on inconsistencies caused by fixpoints in a cartesian closed category
• Coherence for bicategories and indexed categories
• Combinators and functional programming languages. Thirteenth Spring School of the LITP, Val d'Ajol, France, May 6-10, 1985. Proceedings
• The system \({\mathcal F}\) of variable types, fifteen years later
• Normal functors, power series and \(\lambda\)-calculus
• A semantics of multiple inheritance
• The calculus of constructions
• The lambda calculus, its syntax and semantics
• Recursion over realizability structures
• Extensional PERs
• Coherence and consistency in domains
• 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
• Coherence in closed categories
• Models of the lambda calculus
• Operations on records
• What is a model of the lambda calculus?
• 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

This page was built for publication: Inheritance as implicit coercion