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

DOI10.1016/J.APAL.2005.09.001zbMATH Open1099.03011OpenAlexW1976673631MaRDI QIDQ2498898FDOQ2498898

Vincent Balat, Roberto Di Cosmo, Marcelo P. Fiore

Publication date: 16 August 2006

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2005.09.001

zbMATH Keywords

Tarski's high school algebra problemtype isomorphismtyped lambda calculus with sums

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Introduction to extensive and distributive categories
• Introduction to distributive categories
• Retrieving library functions by unifying types modulo linear isomorphism
• Equational theory of positive numbers with exponentiation is not finitely axiomatizable
• Using types as search keys in function libraries
• Provable isomorphisms of types
• An extended arithmetic of ordinal numbers
• On exponentiation -- a solution to Tarski's high school algebra problem
• Equational Theory of Positive Numbers with Exponentiation
• Tarski's High School Identities
• The category of finite sets and Cartesian closed categories
• Left and right adjoint operations on spaces and data types
• Objective number theory and the retract chain condition
• Second order isomorphic types: A proof theoretic study on second order \(\lambda\)-calculus with surjective pairing and terminal object
• Isomorphic objects in symmetric monoidal closed categories

Cited In (10)

• Automorphisms of types in certain type theories and representation of finite groups
• Isomorphic formulae in classical propositional logic
• Relative full completeness for bicategorical Cartesian closed structure
• An intuitionistic formula hierarchy based on high‐school identities
• Second order isomorphic types: A proof theoretic study on second order \(\lambda\)-calculus with surjective pairing and terminal object
• Computing with Semirings and Weak Rig Groupoids
• Title not available (Why is that?)
• Kripke models for classical logic
• On Isomorphisms of Intersection Types
• Isomorphism of intersection and union types

This page was built for publication: Remarks on isomorphisms in typed lambda calculi with empty and sum types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2498898)