# Parametric limits

@article{Dunphy2004ParametricL, title={Parametric limits}, author={Brian P. Dunphy and Uday S. Reddy}, journal={Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.}, year={2004}, pages={242-251} }

We develop a categorical model of polymorphic lambda calculi using the notion of parametric limits, which extend the notion of limits in categories to reflexive graphs of categories. We show that a number of parametric models of polymorphism can be captured in this way. We also axiomatize the structure of reflexive graphs needed for modelling parametric polymorphism based on ideas of fibrations, and show that it leads to proofs of representation results such as the initial algebra and final… Expand

#### 15 Citations

A Relationally Parametric Model of the Calculus of Constructions

- 2012

In this paper, we give the first relationally parametric model of the (extensional) calculus of constructions. Our model remains as simple as traditional PER models of dependent types, but unlike… Expand

Categorical models for Abadi and Plotkin's logic for parametricity

- Computer Science, Mathematics
- Mathematical Structures in Computer Science
- 2005

A logic can be used to reason about parametric models, such that consequences of parametricity that to the authors' knowledge have not been proved before for existing category-theoretic notions of relational parametricy are proved. Expand

A relationally parametric model of dependent type theory

- Computer Science
- POPL 2014
- 2014

This paper constructs parametric models of predicative and impredicative dependent type theory in terms of reflexive graphs, and is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric model of System F to the dependently typed setting. Expand

Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2014

The problems in generalizing homomorphisms to be generalized from functions to relations are explained, the work carried out so far is summarized, and calls for a renewed attempt at addressing the problem. Expand

A General Framework for Relational Parametricity

- Computer Science, Mathematics
- LICS
- 2018

This work develops an abstract framework for relational parametricity that delivers a model expressing Reynolds' theory in a direct and natural way, and offers a novel relationally parametric model of System F (after Orsanigo), which is proof-relevant in the sense that witnesses of relatedness are themselves suitably related. Expand

Internalizing Relational Parametricity in the Extensional Calculus of Constructions

- Mathematics, Computer Science
- CSL
- 2013

The key idea behind the approach is to interpret types as so-called quasi-PERs (or zigzag-complete relations), which enable us to model the symmetry and transitivity of equality while at the same time allowing abstract types with different representations to be equated. Expand

Parametricity for Nested Types and GADTs

- Computer Science
- ArXiv
- 2021

This paper designs a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints, and proves that this model satisfies an appropriate Abstraction Theorem, as well as that it verifies all standard consequences of parametricity in the presence of primitive nested types. Expand

Parametricity for Primitive Nested Types

- Computer Science
- FoSSaCS
- 2021

This paper designs a Hindley-Milner-style calculus with primitives for constructing nested types directly as fixpoints, and proves that the model satisfies an appropriate Abstraction Theorem and verifies all standard consequences of parametricity for primitive nested types. Expand

Freedom for Proofs!

- 2021

Representation independence allows programmers to give different implementations for an abstract interface. Reynolds’ characterization of representation independence for System F uses parametricity,… Expand

An Automata-Theoretic Model of Idealized Algol - (Extended Abstract)

- Computer Science
- ICALP
- 2012

A new model of class-based Algol-like programming languages inspired by automata-theoretic concepts that is able to combine both the state-based and event-based views of objects. Expand

#### References

SHOWING 1-10 OF 31 REFERENCES

Parametricity of Extensionally Collapsed Term Models of Polymorphism and Their Categorical Properties

- Mathematics, Computer Science
- TACS
- 1991

This paper shows the second order minimum model is parametric, and thus enjoys the property of parametric natural models, and gives representation of internal right and left Kan extensions. Expand

A Logic for Parametric Polymorphism

- Computer Science
- TLCA
- 1993

The logic permits the formal presentation and use of relational parametricity, and yields-for example-encodings of initial algebras, final co-algebra and abstract datatypes, with corresponding proof principles of induction, co-induction and simulation. Expand

On Functors Expressible in the Polymorphic Typed Lambda Calculus

- Computer Science, Mathematics
- Inf. Comput.
- 1993

It is shown that if T is such a functor from K to K that there is a weak initial T-algebra and if, in addition, K possesses equalizers of all subsets of its morphism sets, then there is anInitial T- algebra. Expand

Types, Abstractions, and Parametric Polymorphism, Part 2

- Computer Science
- MFPS
- 1991

The concept of relations over sets is generalized to relations over an arbitrary category, and used to investigate the abstraction (or logical-relations) theorem, the identity extension lemma, and… Expand

Reflexive graphs and parametric polymorphism

- Computer Science, Mathematics
- Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science
- 1994

It is proved that if the authors start with a non-parametric model which is left exact and which satisfies a completeness condition corresponding to Ma and Reynolds "suitability for polymorphism", then they can recover a parametric model with the same category of closed types. Expand

Polymorphism is not Set-Theoretic

- Mathematics, Computer Science
- Semantics of Data Types
- 1984

It is proved that the standard set-theoretic model of the ordinary typed lambda calculus cannot be extended to model this language extension in which polymorphic functions can be defined. Expand

Formal parametric polymorphism

- Mathematics
- 1993

A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds' work, the study of parametricity is typically semantic. In this… Expand

Fibrations, logical predicates and indeterminates

- Mathematics, Computer Science
- CST
- 1993

Within the framework of categorical logic/type theory, we provide a category-theoretic account of some logical concepts, i.e. first-order logical predicates for simply typed lambda-calculus,… Expand

Parametricity as a notion of uniformity in reflexive graphs

- Mathematics
- 2002

Uniformity is an important concept in good computer programming practice. Reflexive graph categories provide an abstract setting where uniformity can be characterized as parametric transformations,… Expand

Theorems for free!

- Computer Science
- FPCA
- 1989

From the type of a polymorphic function the authors can derive a theorem that it satisfies, courtesy of Reynolds’ abstraction theorem for the polymorphic lambda calculus, which provides a free source of useful theorems. Expand