A computational view of implicit coercions in type theory

DOI10.1017/S0960129505004901MaRDI QIDQ3372684zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Implicit coercions in type systems
• scientific article; zbMATH DE number 1086673
• Coercive subtyping: theory and implementation
• Coercions in a polymorphic type system
• Coercive subtyping

Cited in

(9)

• Automorphisms of types in certain type theories and representation of finite groups
• Dependent type system with subtyping I: Type level transitivity elimination
• An implementation of LF with coercive subtyping and universes
• A theory of typed coercions and its applications
• scientific article; zbMATH DE number 1765684 (Why is no real title available?)
• COCHIS: stable and coherent implicits
• Equality, quasi-implicit products, and large eliminations
• Nonuniform coercions via unification hints
• Implicit coercions in type systems

Describes a project that uses

Uses Software

• Plastic

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

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