Functorial polymorphism

DOI10.1016/0304-3975(90)90151-7zbMath0717.18005OpenAlexW2914837968MaRDI QIDQ753948

E. S. Bainbridge, Andrej Scedrov, Philip J. Scott, Peter J. Freyd

Publication date: 1990

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

Full work available at URL: https://doi.org/10.1016/0304-3975(90)90151-7

zbMATH Keywords

cartesian closed categoryhigher-order lambda calculussemantic approximations to Strachey's parametric polymorphism

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Combinatory logic and lambda calculus (03B40)

Related Items (48)

Types as parameters ⋮ The Girard-Reynolds isomorphism ⋮ The naturality of natural deduction ⋮ Parametricity as isomorphism ⋮ A principled approach to programming with nested types in Haskell ⋮ Least fixpoints of endofunctors of cartesian closed categories ⋮ Categorical data types in parametric polymorphism ⋮ A categorical semantics for polarized MALL ⋮ Games and full completeness for multiplicative linear logic ⋮ Linear Läuchli semantics ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ Parametricity of extensionally collapsed term models of polymorphism and their categorical properties ⋮ An extension of system F with subtyping ⋮ Covariant types ⋮ The equational logic of fixed points ⋮ Proof Nets, Coends and the Yoneda Isomorphism ⋮ G-dinaturality. ⋮ Types, abstraction, and parametric polymorphism, part 2 ⋮ A representation theorem for second-order functionals ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ A modest model of records, inheritance, and bounded quantification ⋮ Notions of computation as monoids ⋮ Unnamed Item ⋮ Parametricity for primitive nested types ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Fixed-point operations on ccc's. I ⋮ Selective strictness and parametricity in structural operational semantics, inequationally ⋮ A characterization of the least-fixed-point operator by dinaturality ⋮ Linear logic, coherence and dinaturality ⋮ Softness of hypercoherences and MALL full completeness ⋮ Introduction to Type Theory ⋮ Composing dinatural transformations: towards a calculus of substitution ⋮ On paradoxes in normal form ⋮ Unnamed Item ⋮ Game Semantics for Bounded Polymorphism ⋮ On Compositionality of Dinatural Transformations ⋮ Functorial polymorphism ⋮ Unnamed Item ⋮ On the algebraic structure of declarative programming languages ⋮ Inversion, Iteration, and the Art of Dual Wielding ⋮ Dinatural numbers ⋮ A sequent calculus for subtyping polymorphic types ⋮ Event Domains, Stable Functions and Proof-Nets ⋮ Relational Parametricity for Control Considered as a Computational Effect ⋮ Formal parametric polymorphism ⋮ Baby Modula-3 and a theory of objects ⋮ An exactification of the monoid of primitive recursive functions ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

Uses Software

• Miranda
• Nuprl
• Forsythe

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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Extensional models for polymorphism
• The semantics of second-order lambda calculus
• Functorial polymorphism
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The system \({\mathcal F}\) of variable types, fifteen years later
• A small complete category
• CLU reference manual
• The lambda calculus, its syntax and semantics
• LCF considered as a programming language
• On functors expressible in the polymorphic typed lambda calculus
• Fundamental concepts in programming languages
• Edinburgh LCF. A mechanized logic of computation
• 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
• A generalization of the functorial calculus
• Constructive mathematics and computer programming
• The Discrete Objects in the Effective Topos
• Categorical semantics for higher order polymorphic lambda calculus
• The Category-Theoretic Solution of Recursive Domain Equations
• Constructive natural deduction and its ‘ω-set’ interpretation
• Data Types as Lattices
• The next 700 programming languages
• Dinatural transformations

This page was built for publication: Functorial polymorphism