COCHIS: stable and coherent implicits

DOI10.1017/S0956796818000242zbMATH Open1493.68094OpenAlexW2912261953WikidataQ128437207 ScholiaQ128437207MaRDI QIDQ4972074FDOQ4972074

Authors: Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler, Koar Marntirosian 

Publication date: 22 November 2019

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796818000242

Recommendations

• Implicit coercions in type systems
• A computational view of implicit coercions in type theory
• scientific article; zbMATH DE number 1722663
• Implicit parameters: dynamic scoping with static types
• The coherence of languages with intersection types

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Deductive Approach to Program Synthesis
• A theory of type polymorphism in programming
• An Efficient Unification Algorithm
• An extended comparative study of language support for generic programming
• Associated type synonyms
• Associated types with class
• Closed type families with overlapping equations
• Complete and easy bidirectional typechecking for higher-rank polymorphism
• Dependently typed programming in Agda
• FPH: first-class polymorphism for Haskell
• First-Class Type Classes
• Focusing and polarization in linear, intuitionistic, and classical logics
• HMF: simple type inference for first-class polymorphism
• How to make ad hoc proof automation less ad hoc
• Implicit parameters: dynamic scoping with static types
• Inheritance as implicit coercion
• Instance chains: type class programming without overlapping instances
• Logic Programming with Focusing Proofs in Linear Logic
• Logical relations for coherence of effect subtyping
• ML ^F
• Modular type classes
• On the bright side of type classes: instance arguments in Agda
• Practical type inference for arbitrary-rank types
• Propositions as sessions
• Qualified Types
• The Principal Type-Scheme of an Object in Combinatory Logic
• The coherence of languages with intersection types
• The lambda calculus, its syntax and semantics
• Type checking with open type functions
• Types and programing languages
• Understanding functional dependencies via constraint handling rules
• Unification under a mixed prefix
• Uniform proofs as a foundation for logic programming
• \textsc{OutsideIn(X)}: modular type inference with local assumptions

Uses Software

• ML
• Haskell
• GHC
• Scala
• Agda
• Idris
• Rust
• GitHub

This page was built for publication: COCHIS: stable and coherent implicits

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