Remarks on isomorphisms in typed lambda calculi with empty and sum types

Reference. Remarks on isomorphisms in typed lambda calculi with empty and sum types

Marcelo P. Fiore, Roberto Di Cosmo, Vincent Balat · APAL · 2006 · DOI

Cite

Cite as @fiore-2006-remarks (helia, typst) · \cite{fiore-2006-remarks} (LaTeX)

BibTeX

bibtex · 1 line

@article{fiore-2006-remarks, title={Remarks on isomorphisms in typed lambda calculi with empty and sum types}, volume={141}, ISSN={0168-0072}, url={http://dx.doi.org/10.1016/j.apal.2005.09.001}, DOI={10.1016/j.apal.2005.09.001}, number={1-2}, journal={Annals of Pure and Applied Logic}, publisher={Elsevier BV}, author={Fiore, Marcelo and Di Cosmo, Roberto and Balat, Vincent}, year={2006}, month=Aug, pages={35–50} }

hayagriva YAML (typst)

yaml · 19 lines

fiore-2006-remarks:
  type: article
  title: Remarks on isomorphisms in typed lambda calculi with empty and sum types
  author:
  - Fiore, Marcelo
  - Di Cosmo, Roberto
  - Balat, Vincent
  date: 2006-08
  page-range: 35-50
  url: http://dx.doi.org/10.1016/j.apal.2005.09.001
  serial-number:
    doi: 10.1016/j.apal.2005.09.001
    issn: 0168-0072
  parent:
    type: periodical
    title: Annals of Pure and Applied Logic
    publisher: Elsevier BV
    issue: 1–2
    volume: 141

Download: fiore-2006-remarks.bib · fiore-2006-remarks.yml

Cited by (2)

Fractional Types: Expressive and Safe Space Management for Ancilla Bits chen-2020-fractionalRC · 2020

DOI · arXiv

Relational algebra by way of adjunctions gibbons-2018-relationalICFP · 2018

Bulk types such as sets, bags, and lists are monads, and therefore support a notation for database queries based on comprehensions. This fact is the basis of much work on database query languages. The monadic structure easily explains most of standard relational algebra—specifically, selections and projections—allowing for an elegant mathematical foundation for those aspects of database query language design. Most, but not all: monads do not immediately offer an explanation of relational join or grouping, and hence important foundations for those crucial aspects of relational algebra are missing. The best they can offer is cartesian product followed by selection. Adjunctions come to the rescue: like any monad, bulk types also arise from certain adjunctions; we show that by paying due attention to other important adjunctions, we can elegantly explain the rest of standard relational algebra. In particular, graded monads provide a mathematical foundation for indexing and grouping, which leads directly to an efficient implementation, even of joins.

PDF · DOI · pldb

Cites 31 works (1 here)

With notes (1)

Introduction to Higher-Order Categorical Logic lambek_scott_19861986

Web

External (30)

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums (2004)
Left and right adjoint operations on spaces and data types (2004)
Extensional normalisation for typed lambda calculus with sums via Grothendieck logical relations (manuscript) (2002)
Type isomorphisms and proof reuse in dependent type theory (2001)
Objective number theory and the retract chain condition (2000)
Transcendence in objective number theory (2000)
A linear logical view of linear type isomorphisms (1999)
Isomorphic objects in symmetric monoidal closed categories (1997)
Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes (1997)
Type isomorphisms for module signatures (1996)
Second order isomorphic types. A proof theoretic study on second order λ-calculus with surjective pairing and terminal object (1995)
Isomorphisms of Types: from λ-Calculus to Information Retrieval and Language Design (1995)
Tarski’s high school identities (1993)
Introduction to extensive and distributive categories (1993)
Introduction to distributive categories (1993)
Deciding type isomorphisms in a type assignment framework (1993)
A complete axiom system for isomorphism of types in closed categories (1993)
Provable isomorphisms of types (1992)
Type isomorphisms in a type assignment framework (1992)
Using types as search keys in function libraries (1991)
Retrieving re-usable software components by polymorphic type (1991)
Equational theory of positive numbers with exponentiation is not finitely axiomatizable (1990)
Retrieving library identifiers by equational matching of types (1990)
Searching program libraries by type and proving compiler correctness by bisimulation (PhD thesis) (1990)
Provable isomorphisms and domain equations in models of typed languages (1985)
Equational theory of positive numbers with exponentiation (1985)
The category of finite sets and cartesian closed categories (1983)
On exponentiation — A solution to Tarski's high school algebra problem (preprint) (1981)
Axiomatic bases for equational theories of natural numbers (1972)
An extended arithmetic of ordinal numbers (1969)