A computational view of implicit coercions in type theory

DOI10.1017/S0960129505004901zbMath1084.68023OpenAlexW2020431458MaRDI QIDQ3372684

Gilles Barthe

Publication date: 10 March 2006

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129505004901

zbMATH Keywords

back-and-forth coercions

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Dependent type system with subtyping I: Type level transitivity elimination ⋮ Automorphisms of types in certain type theories and representation of finite groups

Uses Software

• Plastic

This page was built for publication: A computational view of implicit coercions in type theory