Functorial polymorphism
From MaRDI portal
The authors study two semantic approximations to Strachey's parametric polymorphism. The first one insists on certain naturality conditions on indexed families of functions and therefore interprets universal type abstraction as only a part of the product over all types. Types are approximated by functors and terms by natural transformations between types, all defined over some cartesian closed category of ``ground types. The second approximation is based on a version of Reynold's invariance condition.
Recommendations
Cites work
- A generalization of the functorial calculus
- A small complete category
- Automatic synthesis of typed -programs on term algebras
- Categorical semantics for higher order polymorphic lambda calculus
- CLU reference manual
- Constructive mathematics and computer programming
- Constructive natural deduction and its ‘ω-set’ interpretation
- Data Types as Lattices
- Dinatural transformations
- Domain theoretic models of polymorphism
- Edinburgh LCF. A mechanized logic of computation
- Extensional models for polymorphism
- Functorial polymorphism
- Fundamental concepts in programming languages
- scientific article; zbMATH DE number 4181330 (Why is no real title available?)
- scientific article; zbMATH DE number 3882404 (Why is no real title available?)
- scientific article; zbMATH DE number 4158597 (Why is no real title available?)
- scientific article; zbMATH DE number 3825806 (Why is no real title available?)
- scientific article; zbMATH DE number 3902022 (Why is no real title available?)
- scientific article; zbMATH DE number 3928956 (Why is no real title available?)
- scientific article; zbMATH DE number 3951980 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 4033057 (Why is no real title available?)
- scientific article; zbMATH DE number 4049849 (Why is no real title available?)
- scientific article; zbMATH DE number 4050971 (Why is no real title available?)
- scientific article; zbMATH DE number 4061468 (Why is no real title available?)
- scientific article; zbMATH DE number 3763259 (Why is no real title available?)
- scientific article; zbMATH DE number 3780545 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 195199 (Why is no real title available?)
- scientific article; zbMATH DE number 3261673 (Why is no real title available?)
- scientific article; zbMATH DE number 3379785 (Why is no real title available?)
- scientific article; zbMATH DE number 3384257 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- LCF considered as a programming language
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- On functors expressible in the polymorphic typed lambda calculus
- The Category-Theoretic Solution of Recursive Domain Equations
- The Discrete Objects in the Effective Topos
- The lambda calculus, its syntax and semantics
- The next 700 programming languages
- The semantics of second-order lambda calculus
- The system \({\mathcal F}\) of variable types, fifteen years later
Cited in
(62)- On the algebraic structure of declarative programming languages
- Dinatural numbers
- Formal parametric polymorphism
- Parametricity as isomorphism
- Covariant types
- The equational logic of fixed points
- G-dinaturality.
- A sequent calculus for subtyping polymorphic types
- The Girard-Reynolds isomorphism
- Linear Läuchli semantics
- Composing dinatural transformations: towards a calculus of substitution
- The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
- Parametricity for primitive nested types
- On paradoxes in normal form
- Selective strictness and parametricity in structural operational semantics, inequationally
- The naturality of natural deduction
- Game semantics for bounded polymorphism
- Functors are type refinement systems
- Event domains, stable functions and proof-nets
- Functorial semantics of first-order views
- scientific article; zbMATH DE number 4154448 (Why is no real title available?)
- Bunched polymorphism
- Functorial ML
- Least fixpoints of endofunctors of cartesian closed categories
- Categorical data types in parametric polymorphism
- Games and full completeness for multiplicative linear logic
- Notions of computation as monoids
- Polymorphism and the obstinate circularity of second order logic: a victims' tale
- Baby Modula-3 and a theory of objects
- Proof nets, coends and the Yoneda isomorphism
- Parametricity for nested types and GADTs
- Types as parameters
- On Compositionality of Dinatural Transformations
- Parametricity of extensionally collapsed term models of polymorphism and their categorical properties
- An extension of system \(F\) with subtyping
- scientific article; zbMATH DE number 7204448 (Why is no real title available?)
- Introduction to Type Theory
- Inversion, iteration, and the art of dual wielding
- Relational parametricity for control considered as a computational effect
- A representation theorem for second-order functionals
- General Homomorphic Overloading
- Bifibrational functorial semantics of parametric polymorphism
- Types, abstraction, and parametric polymorphism, part 2
- A logical aspect of parametric polymorphism
- Intensional harmony as isomorphism
- Fixed-point operations on ccc's. I
- Revisiting decidable bounded quantification, via dinaturality
- The Yoneda reduction of polymorphic types
- A characterization of the least-fixed-point operator by dinaturality
- Structural polymorphism
- Linear logic, coherence and dinaturality
- Deduction at the crossroads
- A new conjecture about identity of proofs
- A logical approach to type soundness
- Softness of hypercoherences and MALL full completeness
- Functorial polymorphism
- An exactification of the monoid of primitive recursive functions
- A principled approach to programming with nested types in Haskell
- A categorical semantics for polarized MALL
- Core algebra revisited
- The Girard-Reynolds isomorphism (second edition)
- A modest model of records, inheritance, and bounded quantification
This page was built for publication: Functorial polymorphism
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q753948)
