Implicit coercions in type systems

DOI10.1007/3-540-61780-9_58MaRDI QIDQ4647565zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

formal systemnormal formrecord typetype systemtype theory

Mathematics Subject Classification ID

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

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

Cites work

• A system of constructor classes: overloading and implicit higher-order polymorphism
• scientific article; zbMATH DE number 4054988 (Why is no real title available?)
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 615137 (Why is no real title available?)
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Subtyping dependent types
• Typing in pure type systems

Cited in

(14)

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

Describes a project that uses

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)