A computational view of implicit coercions in type theory

DOI10.1017/S0960129505004901zbMATH Open1084.68023OpenAlexW2020431458MaRDI QIDQ3372684FDOQ3372684

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

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

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)

Cited In (9)

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

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)