# Notes on Sconing and Relators

@inproceedings{Mitchell1992NotesOS, title={Notes on Sconing and Relators}, author={John C. Mitchell and Andre Scedrov}, booktitle={CSL}, year={1992} }

This paper describes a semantics of typed lambda calculi based on relations. The main mathematical tool is a category-theoretic method of sconing, also called glueing or Freyd covers. Its correspondence to logical relations is also examined.

#### Topics from this paper

#### 71 Citations

A Characterization of lambda Definability in Categorical Models of Implicit Polymorphism

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 1995

A category-theoretic framework known as glueing or sconing is used to extend the Jung-Tiuryn (1993) characterization of lambda definability first to ccc models, and then to categorical models of the calculus with type variables. Expand

Under Consideration for Publication in J. Functional Programming Girard Translation and Logical Predicates

- 2000

We present a short proof of a folklore result: the Girard translation from the simply typed lambda calculus to the linear lambda calculus is fully complete. The proof makes use of a notion of logical… Expand

Parametric limits

- Computer Science
- Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.
- 2004

A categorical model of polymorphic lambda calculi is developed using the notion of parametric limits, which extend the idea of limits in categories to reflexive graphs of categories and axiomatize the structure of Reflexive graphs needed for modelling parametric polymorphism. Expand

Parametric limits

- Mathematics
- LICS 2004
- 2004

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… Expand

Relating Computational Effects by ⊤ ⊤-Lifting

- Computer Science, Mathematics
- ICALP
- 2011

We consider the problem of establishing a relationship between two interpretations of base type terms of a λc-calculus with algebraic operations. We show that the given relationship holds if it… Expand

Logical Relations for Monadic Types

- Computer Science
- CSL
- 2002

This work proposes a natural notion of logical relations able to deal with the monadic types of Moggi's computational lambda-calculus, based on notions of subsconing and distributivity laws for monads. Expand

Logical Predicates for Intuitionistic Linear Type Theories

- Mathematics, Computer Science
- TLCA
- 1999

A notion of Kripke-like parameterized logical predicates for two fragments of intuitionistic linear logic in terms of their category-theoretic models are developed, derived from the categorical glueing construction combined with the free symmetric monoidal cocompletion. Expand

Kripke Logical Relations and PCF

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

It is shown that one may achieve full abstraction at all types using a form of "Kripke logical relations" introduced by Jung and Tiuryn to characterize λ-definability. Expand

University of Birmingham Parametric limits

- 2004

We develop a categorical model of polymorphic lambda calculi using a notion called parametric limits, which extend the notion of limits in categories to reexive graphs of categories. We show that a… Expand

Logical relations for monadic types†

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

This work proposes a natural notion of logical relations that is able to deal with the monadic types of Moggi's computational lambda calculus, and is based on notions of subsconing, mono factorisation systems and monad morphisms. Expand

#### References

SHOWING 1-10 OF 59 REFERENCES

A relational approach to strictness analysis for higher-order polymorphic functions

- Computer Science
- POPL '91
- 1991

This paper defines the categorical notions of relators and transformations and shows that these concepts enable us to give a semantics for polymorphic, higher order functional programs and proves that strictness analysis is a polymorphic invariant. Expand

Computational lambda-calculus and monads

- Mathematics, Computer Science
- [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science
- 1989

The author gives a calculus based on a categorical semantics for computations, which provides a correct basis for proving equivalence of programs, independent from any specific computational model. Expand

Categorical Semantics for Higher Order Polymorphic Lambda Calculus

- Mathematics, Computer Science
- J. Symb. Log.
- 1987

On definit une structure categorique adaptee a l'interpretation du lambda-calcul polymorphe, qui fournit une semantique algebrique solide et complete

Logical Relations and the Typed lambda-Calculus

- Computer Science, Mathematics
- Inf. Control.
- 1985

Demonstration des principaux resultats syntaxiques sur le calcul de type lambda a partir du theoreme fondamental des relations logiques. 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

Proofs and types

- Mathematics
- 1989

Sense, denotation and semantics natural deduction the Curry-Howard isomorphism the normalisation theorem Godel's system T coherence spaces denotational semantics of T sums in natural deduction system… Expand

Extensional Models for Polymorphism

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 1988

The polymorphic extensional collapse method yields models that prove that the polymorphic lambda calculus can be conservatively added to arbitrary algebraic data type specifications, even with complete transfer of the computational power to the added data types. 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

On the Relation between Direct and Continuation Semantics

- Computer Science
- ICALP
- 1974

This work gives two theorems which specify the relationship between the direct and the continuation semantic functions for a purely applicative language and shows that direct semantics are included in continuation semantics. Expand

An Extension of System F with Subtyping

- Computer Science
- TACS
- 1991

The main focus of the paper is the equational theory of F<:, which is related to PER models and the notion of parametricity, and some categorical properties of the theory when restricted to closed terms, including interesting categorical isomorphisms. Expand