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

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 1696585 (Why is no real title available?)
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 445160 (Why is no real title available?)
• 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

Describes a project that uses

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)