Implicit coercions in type systems

DOI10.1007/3-540-61780-9_58zbMath1434.03081OpenAlexW2129022339MaRDI QIDQ4647565

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 formformal systemtype systemtype theoryrecord type

Mathematics Subject Classification ID

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

Related Items

Validating Mathematical Structures, Working with Mathematical Structures in Type Theory, A constructive algebraic hierarchy in Coq., 2-Dimensional Directed Type Theory

Uses Software

• Haskell
• Automath

Cites Work

• Typing in pure type systems
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A system of constructor classes: overloading and implicit higher-order polymorphism
• Subtyping dependent types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item