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

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)

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

• 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?)
• A system of constructor classes: overloading and implicit higher-order polymorphism
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Subtyping dependent types
• 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
• scientific article; zbMATH DE number 814794 (Why is no real title available?)
• 2-Dimensional Directed Type Theory
• Nonuniform coercions via unification hints

Describes a project that uses

Uses Software

• Automath
• Haskell

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)