Implicit coercions in type systems

DOI10.1007/3-540-61780-9_58zbMATH Open1434.03081OpenAlexW2129022339MaRDI QIDQ4647565FDOQ4647565

Authors: Gilles Barthe 

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/2181

Recommendations

• A computational view of implicit coercions in type theory
• Coercions in a polymorphic type system
• Types for Proofs and Programs
• Coercive subtyping
• scientific article; zbMATH DE number 814794

zbMATH Keywords

normal formtype theorytype systemformal systemrecord type

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Type theory (03B38)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Subtyping dependent types
• Title not available (Why is that?)
• Title not available (Why is that?)
• A system of constructor classes: overloading and implicit higher-order polymorphism
• Typing in pure type systems

Cited In (13)

• Implicit typing à la ML for the join-calculus
• Transitivity in coercive subtyping
• A constructive algebraic hierarchy in Coq.
• Integrating coercion with subtyping and multiple dispatch
• Is Impredicativity Implicitly Implicit
• COCHIS: stable and coherent implicits
• A computational view of implicit coercions in type theory
• Validating Mathematical Structures
• Coercions in a polymorphic type system
• Working with Mathematical Structures in Type Theory
• Title not available (Why is that?)
• 2-Dimensional Directed Type Theory
• Nonuniform coercions via unification hints

Uses Software

• Haskell
• Automath

This page was built for publication: Implicit coercions in type systems

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