bibliography.bib

@article{LinearHaskell,
 author = {Bernardy, Jean-Philippe and Boespflug, Mathieu and Newton, Ryan R. and Peyton Jones, Simon and Spiwack, Arnaud},
 title = {Linear Haskell: Practical Linearity in a Higher-order Polymorphic Language},
 journal = {Proc. ACM Program. Lang.},
 issue_date = {January 2018},
 volume = {2},
 number = {POPL},
 month = dec,
 year = {2017},
 issn = {2475-1421},
 pages = {5:1--5:29},
 articleno = {5},
 numpages = {29},
 url = {http://doi.acm.org/10.1145/3158093},
 doi = {10.1145/3158093},
 acmid = {3158093},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {GHC, Haskell, laziness, linear logic, linear types, polymorphism, typestate},
}

@article{OutsideIn,
 title={OutsideIn(X) Modular type inference with local assumptions},
 volume={21},
 url = {http://doi.acm.org/10.1017/S0956796811000098},
 doi={10.1017/S0956796811000098},
 number={4-5},
 journal={Journal of Functional Programming},
 publisher={Cambridge University Press},
 author={Vytiniotis, Dimitrios and Peyton Jones, Simon and Schrijvers, Tom and Sulzmann, Martin},
 year={2011},
 pages={333–412}
}

@article{resource-management-for-ll-proof-search,
title = "Efficient resource management for linear logic proof search",
journal = "Theoretical Computer Science",
volume = "232",
number = "1",
pages = "133 - 163",
year = "2000",
issn = "0304-3975",
doi = "10.1016/S0304-3975(99)00173-5",
url = "https://doi.org/10.1016/S0304-3975(99)00173-5",
author = "Iliano Cervesato and Joshua S. Hodas and Frank Pfenning",
keywords = "Linear logic, Theorem proving, Logic programming",
abstract = "The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and hereditary Harrop formulas (λProlog and Elf). Among these, the problem of efficiently managing the linear context when solving a goal is of crucial importance for the use of these systems in non-trivial applications. This paper studies this problem in the case of Lolli [10], though its results have application to other systems including those based on linear type theory. We first give a proof-theoretic presentation of the operational semantics of this language as a resolution calculus. We then present a series of resource management systems designed to eliminate the non-determinism in the distribution of linear formulas that undermines the efficiency of a direct implementation of this system."
}

@article{hh-ll,
title = "Logic Programming in a Fragment of Intuitionistic Linear Logic",
journal = "Information and Computation",
volume = "110",
number = "2",
pages = "327 - 365",
year = "1994",
issn = "0890-5401",
doi = "inco.1994.1036",
url = "https://doi.org/10.1006/inco.1994.1036",
author = "J.S. Hodas and D. Miller",
abstract = "When logic programming is based on the proof theory of intuitionistic logic, it is natural to allow implications in goals and in the bodies of clauses. Attempting to prove a goal of the form D ⊃ G from the context (set of formulas) Γ leads to an attempt to prove the goal G in the extended context Γ ∪ {D}. Thus contexts, represented as the left-hand side of intuitionistic sequents, grow as stacks during the bottom-up search for a cut-free proof. While such an intuitionistic notion of context provides for elegant specifications of many computations, contexts can be made more expressive and flexible if they are based on linear logic. After presenting two equivalent formulations of a fragment of linear logic, we show that the fragment has a goal-directed interpretation, thereby partially justifying calling it a logic program-ming language. Logic programs based on the intuitionistic theory of hereditary Harrop formulas can be modularly embedded into this linear logic setting. Programming examples taken from theorem proving, natural language parsing, and data base programming are presented: each example requires a linear, rather than intuitionistic, notion of context to be modeled adequately. An interpreter for this logic programming language must address the problem of splitting contexts; that is, in the attempt to prove a multiplicative conjunction (tensor), say G1 ⊗ G2, from the context Δ the latter must be split into disjoint contexts Δ1 and Δ2 for which G1 follows from Δ1 and G2 follows from Δ2. Since there is an exponential number of such splits, it is important to delay the choice of a split as much as possible. A mechanism for the lazy splitting of contexts is presented based on viewing proof search as a process that takes a context, consumes part of it, and returns the rest (to be consumed elsewhere). In addition, we use collections of Kripke interpretations indexed by a commutative monoid to provide models for this logic programming language and show that logic programs admit canonical models."
}

@misc{shulman2018linear,
      title={Linear logic for constructive mathematics},
      author={Michael Shulman},
      year={2018},
      eprint={1805.07518},
      archivePrefix={arXiv},
      primaryClass={math.LO}
}

@InProceedings{AtsLinearViews,
author="Zhu, Dengping
and Xi, Hongwei",
editor="Hermenegildo, Manuel V.
and Cabeza, Daniel",
title="Safe Programming with Pointers Through Stateful Views",
booktitle="Practical Aspects of Declarative Languages",
year="2005",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="83--97",
abstract="The need for direct memory manipulation through pointers is essential in many applications. However, it is also commonly understood that the use (or probably misuse) of pointers is often a rich source of program errors. Therefore, approaches that can effectively enforce safe use of pointers in programming are highly sought after. ATS is a programming language with a type system rooted in a recently developed framework Applied Type System, and a novel and desirable feature in ATS lies in its support for safe programming with pointers through a novel notion of stateful views. In particular, even pointer arithmetic is allowed in ATS and guaranteed to be safe by the type system of ATS. In this paper, we give an overview of this feature in ATS, presenting some interesting examples based on a prototype implementation of ATS to demonstrate the practicality of safe programming with pointer through stateful views.",
isbn="978-3-540-30557-6"
}

@article{QualifiedTypes,
title = "A theory of qualified types",
journal = "Science of Computer Programming",
volume = "22",
number = "3",
pages = "231 - 256",
year = "1994",
issn = "0167-6423",
doi = "10.1016/0167-6423(94)00005-0",
url = "https://doi.org/10.1016/0167-6423(94)00005-0",
author = "Mark P. Jones",
abstract = "This paper describes a general theory of overloading based on a system of qualified types. The central idea is the use of predicates in the type of a term, restricting the scope of universal quantification. A corresponding semantic notion of evidence is introduced and provides a uniform framework for implementing applications of this system, including Haskell style type classes, extensible records and subtyping. Working with qualified types in a simple, implicitly typed, functional language, we extend the Damas-Milner approach to type inference. As a result, we show that the set of all possible typings for a given term can be characterized by a principal type scheme, calculated by a type inference algorithm."
}

@article{altenkirch2010quantum,
  title={The quantum IO monad},
  author={Altenkirch, Thorsten and Green, Alexander S},
  journal={Semantic Techniques in Quantum Computation},
  pages={173--205},
  year={2010},
  publisher={Cambridge University Press}
}

@inproceedings{quantified-constraints,
author = {Bottu, Gert-Jan and Karachalias, Georgios and Schrijvers, Tom and Oliveira, Bruno C. d. S. and Wadler, Philip},
title = {Quantified Class Constraints},
year = {2017},
isbn = {9781450351829},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3122955.3122967},
doi = {10.1145/3122955.3122967},
abstract = {Quantified class constraints have been proposed many years ago to raise the expressive power of type classes from Horn clauses to the universal fragment of Hereditiary Harrop logic. Yet, while it has been much asked for over the years, the feature was never implemented or studied in depth. Instead, several workarounds have been proposed, all of which are ultimately stopgap measures. This paper revisits the idea of quantified class constraints and elaborates it into a practical language design. We show the merit of quantified class constraints in terms of more expressive modeling and in terms of terminating type class resolution. In addition, we provide a declarative specification of the type system as well as a type inference algorithm that elaborates into System F. Moreover, we discuss termination conditions of our system and also provide a prototype implementation.},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell},
pages = {148–161},
numpages = {14},
keywords = {Haskell, type classes, type inference},
location = {Oxford, UK},
series = {Haskell 2017}
}

@inproceedings{mezzo-permissions,
author = {Pottier, Fran\c{c}ois and Protzenko, Jonathan},
title = {Programming with Permissions in Mezzo},
year = {2013},
isbn = {9781450323260},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2500365.2500598},
doi = {10.1145/2500365.2500598},
abstract = {We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. This rules out certain mistakes, including representation exposure and data races, and enables new idioms, such as gradual initialization, memory re-use, and (type)state changes. Although the core static discipline disallows sharing a mutable data structure, Mezzo offers several ways of working around this restriction, including a novel dynamic ownership control mechanism which we dub "adoption and abandon".},
booktitle = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
pages = {173–184},
numpages = {12},
keywords = {side effects, ownership, aliasing, static type systems},
location = {Boston, Massachusetts, USA},
series = {ICFP '13}
}

@InProceedings{liquid-haskell-abstract-refinement-types,
author="Vazou, Niki
and Rondon, Patrick M.
and Jhala, Ranjit",
editor="Felleisen, Matthias
and Gardner, Philippa",
title="Abstract Refinement Types",
booktitle="Programming Languages and Systems",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="209--228",
abstract="We present abstract refinement types which enable quantification over the refinements of data- and function-types. Our key insight is that we can avail of quantification while preserving SMT-based decidability, simply by encoding refinement parameters as uninterpreted propositions within the refinement logic. We illustrate how this mechanism yields a variety of sophisticated means for reasoning about programs, including: parametric refinements for reasoning with type classes, index-dependent refinements for reasoning about key-value maps, recursive refinements for reasoning about recursive data types, and inductive refinements for reasoning about higher-order traversal routines. We have implemented our approach in a refinement type checker for Haskell and present experiments using our tool to verify correctness invariants of various programs.",
isbn="978-3-642-37036-6"
}

@article{ats-lang,
  author    = {Hongwei Xi},
  title     = {Applied Type System: An Approach to Practical Programming with Theorem-Proving},
  journal   = {CoRR},
  volume    = {abs/1703.08683},
  year      = {2017},
  url       = {http://arxiv.org/abs/1703.08683},
  archivePrefix = {arXiv},
  eprint    = {1703.08683},
  timestamp = {Mon, 13 Aug 2018 16:47:04 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/Xi17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{10.1145/773473.178246,
author = {Launchbury, John and Peyton Jones, Simon L.},
title = {Lazy Functional State Threads},
year = {1994},
issue_date = {June 1994},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {29},
number = {6},
issn = {0362-1340},
url = {https://doi.org/10.1145/773473.178246},
doi = {10.1145/773473.178246},
abstract = {Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language.The security of the encapsulation is assured by the type system, using parametricity. Intriguingly, this parametricity requires the provision of a (single) constant with a rank-2 polymorphic type.},
journal = {SIGPLAN Not.},
month = jun,
pages = {24–35},
numpages = {12}
}

@inproceedings{st-monad,
author = {Launchbury, John and Peyton Jones, Simon L.},
title = {Lazy Functional State Threads},
year = {1994},
isbn = {089791662X},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/178243.178246},
doi = {10.1145/178243.178246},
abstract = {Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating stateful computations that manipulate multiple, named, mutable objects, in the context of a non-strict, purely-functional language.The security of the encapsulation is assured by the type system, using parametricity. Intriguingly, this parametricity requires the provision of a (single) constant with a rank-2 polymorphic type.},
booktitle = {Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation},
pages = {24–35},
numpages = {12},
location = {Orlando, Florida, USA},
series = {PLDI '94}
}

@inproceedings{type-class-reflection,
author = {Kiselyov, Oleg and Shan, Chung-chieh},
title = {Functional Pearl: Implicit Configurations--or, Type Classes Reflect the Values of Types},
year = {2004},
isbn = {1581138504},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1017472.1017481},
doi = {10.1145/1017472.1017481},
abstract = {The configurations problem is to propagate run-time preferences throughout a program, allowing multiple concurrent configuration sets to coexist safely under statically guaranteed separation. This problem is common in all software systems, but particularly acute in Haskell, where currently the most popular solution relies on unsafe operations and compiler pragmas.We solve the configurations problem in Haskell using only stable and widely implemented language features like the type-class system. In our approach, a term expression can refer to run-time configuration parameters as if they were compile-time constants in global scope. Besides supporting such intuitive term notation and statically guaranteeing separation, our solution also helps improve the program's performance by transparently dispatching to specialized code at run-time. We can propagate any type of configuration data-numbers, strings, IO actions, polymorphic functions, closures, and abstract data types. No previous approach to propagating configurations implicitly in any language provides the same static separation guarantees.The enabling technique behind our solution is to propagate values via types, with the help of polymorphic recursion and higher-rank polymorphism. The technique essentially emulates local type-class instance declarations while preserving coherence. Configuration parameters are propagated throughout the code implicitly as part of type inference rather than explicitly by the programmer. Our technique can be regarded as a portable, coherent, and intuitive alternative to implicit parameters. It motivates adding local instances to Haskell, with a restriction that salvages principal types.},
booktitle = {Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell},
pages = {33–44},
numpages = {12},
keywords = {higher-rank polymorphism, polymorphic recursion, existential types, implicit parameters, type classes},
location = {Snowbird, Utah, USA},
series = {Haskell '04}
}@inproceedings{10.1145/2628136.2628141,
author = {Breitner, Joachim and Eisenberg, Richard A. and Peyton Jones, Simon and Weirich, Stephanie},
title = {Safe Zero-Cost Coercions for Haskell},
year = {2014},
isbn = {9781450328739},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2628136.2628141},
doi = {10.1145/2628136.2628141},
abstract = {Generative type abstractions -- present in Haskell, OCaml, and other languages -- are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.},
booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
pages = {189–202},
numpages = {14},
keywords = {newtype deriving, coercion, type class, haskell},
location = {Gothenburg, Sweden},
series = {ICFP '14}
}

@article{safe-coercions,
author = {Breitner, Joachim and Eisenberg, Richard A. and Peyton Jones, Simon and Weirich, Stephanie},
title = {Safe Zero-Cost Coercions for Haskell},
year = {2014},
issue_date = {September 2014},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {49},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/2692915.2628141},
doi = {10.1145/2692915.2628141},
abstract = {Generative type abstractions -- present in Haskell, OCaml, and other languages -- are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.},
journal = {SIGPLAN Not.},
month = aug,
pages = {189–202},
numpages = {14},
keywords = {coercion, haskell, newtype deriving, type class}
}

@article{girard-linear-logic,
title = {Linear logic},
journal = {Theoretical Computer Science},
volume = {50},
number = {1},
pages = {1-101},
year = {1987},
issn = {0304-3975},
doi = {10.1016/0304-3975(87)90045-4},
url = {https://doi.org/10.1016/0304-3975(87)90045-4},
author = {Jean-Yves Girard},
abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.}
}

@inproceedings{ghica_bounded_2014,
  author    = {Dan R. Ghica and
               Alex I. Smith},
  title     = {Bounded Linear Types in a Resource Semiring},
  booktitle = {Programming Languages and Systems - 23rd European Symposium on Programming,
               {ESOP} 2014, Held as Part of the European Joint Conferences on Theory
               and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13,
               2014, Proceedings},
  pages     = {331--350},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-642-54833-8_18},
  doi       = {10.1007/978-3-642-54833-8_18},
  timestamp = {Sun, 23 Mar 2014 10:48:25 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/esop/GhicaS14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{system-fc,
author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Peyton Jones, Simon and Donnelly, Kevin},
title = {System F with Type Equality Coercions},
year = {2007},
isbn = {159593393X},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1190315.1190324},
doi = {10.1145/1190315.1190324},
abstract = {We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric type functions, given meaning by top-level equality axioms. Unlike System F, FC is expressive enough to serve as a target for several different source-language features, including Haskell's newtype, generalised algebraic data types, associated types, functional dependencies, and perhaps more besides.},
booktitle = {Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation},
pages = {53–66},
numpages = {14},
keywords = {typed intermediate language, advanced type features},
location = {Nice, Nice, France},
series = {TLDI '07}
}

@inproceedings{variables-in-patterns,
author = {Eisenberg, Richard A. and Breitner, Joachim and Peyton Jones, Simon},
title = {Type Variables in Patterns},
year = {2018},
isbn = {9781450358354},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3242744.3242753},
doi = {10.1145/3242744.3242753},
abstract = {For many years, GHC has implemented an extension to Haskell that allows type variables to be bound in type signatures and patterns, and to scope over terms. This extension was never properly specified. We rectify that oversight here. With the formal specification in hand, the otherwise-labyrinthine path toward a design for binding type variables in patterns becomes blindingly clear. We thus extend ScopedTypeVariables to bind type variables explicitly, obviating the Proxy workaround to the dustbin of history.},
booktitle = {Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell},
pages = {94–105},
numpages = {12},
keywords = {Haskell, type variables, polymorphism, Patterns},
location = {St. Louis, MO, USA},
series = {Haskell 2018}
}

@unpublished{linear-inline-java,
author = {Facundo Domínguez},
title = {Safe memory management in inline-java using linear types},
note = {Blog post},
year = {2020},
url = {https://web.archive.org/web/20200926082552/https://www.tweag.io/blog/2020-02-06-safe-inline-java/}
}

@article{essence-of-ml-type-inference,
  title={The essence of ML type inference},
  author={Pottier, Fran{\c{c}}ois and R{\'e}my, Didier},
  year={2005},
  publisher={Advanced Topics in Types and Programming Languages}
}

@inproceedings{let-should-not-be-generalised,
  title        = {Let Should Not Be Generalized},
  author       = {Vytiniotis, Dimitrios and Peyton Jones, Simon and Schrijvers, Tom},
  year         = 2010,
  booktitle    = {Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation},
  location     = {Madrid, Spain},
  publisher    = {Association for Computing Machinery},
  address      = {New York, NY, USA},
  series       = {TLDI '10},
  pages        = {39–50},
  doi          = {10.1145/1708016.1708023},
  isbn         = 9781605588919,
  url          = {https://doi.org/10.1145/1708016.1708023},
  abstract     = {From the dawn of time, all derivatives of the classic Hindley-Milner type system have supported implicit generalisation of local let-bindings. Yet, as we will show, for more sophisticated type systems implicit let-generalisation imposes a disproportionate complexity burden. Moreover, it turns out that the feature is very seldom used, so we propose to eliminate it. The payoff is a substantial simplification, both of the specification of the type system, and of its implementation.},
  numpages     = 12,
  keywords     = {generalized algebraic data types, type inference, type families, type classes, haskell}
}

@article{existentials,
author = {Eisenberg, Richard A. and Duboc, Guillaume and Weirich, Stephanie and Lee, Daniel},
title = {An Existential Crisis Resolved: Type inference for first-class existential types},
year = {2021},
issue_date = {August 2021},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {5},
number = {ICFP},
journal = {Proc. ACM Program. Lang.}
}

@inproceedings{deferred-type-errors,
author = {Vytiniotis, Dimitrios and Peyton Jones, Simon and Magalh\~{a}es, Jos\'{e} Pedro},
title = {Equality Proofs and Deferred Type Errors: A Compiler Pearl},
year = {2012},
isbn = {9781450310543},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2364527.2364554},
doi = {10.1145/2364527.2364554},
abstract = {The Glasgow Haskell Compiler is an optimizing compiler that expresses and manipulates
first-class equality proofs in its intermediate language. We describe a simple, elegant
technique that exploits these equality proofs to support deferred type errors. The
technique requires us to treat equality proofs as possibly-divergent terms; we show
how to do so without losing either soundness or the zero-overhead cost model that
the programmer expects.},
booktitle = {Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming},
pages = {341–352},
numpages = {12},
keywords = {type equalities, system fc, deferred type errors},
location = {Copenhagen, Denmark},
series = {ICFP '12}
}


@article{practical-type-inference,
  title =        {Practical type inference for arbitrary-rank types},
  volume =       17,
  doi =          {10.1017/S0956796806006034},
  url = {https://doi.org/10.1017/S0956796806006034},
  number =       1,
  journal =      {Journal of Functional Programming},
  publisher =    {Cambridge University Press},
  author =       {Peyton Jones, Simon and Vytiniotis, Dimitrios and
                  Weirich, Stephanie and Shields, Mark},
  year =         2007,
  pages =        {1–82}
}

@Book{tapl,
  Title                    = {Types and Programming Languages},
  Author                   = {Pierce, Benjamin C.},
  Publisher                = {MIT Press},
  Year                     = {2002},

  Address                  = {Cambridge, MA},

  Owner                    = {rae},
  Timestamp                = {2016.06.28}
}

@InProceedings{visible-type-application,
author="Eisenberg, Richard A.
and Weirich, Stephanie
and Ahmed, Hamidhasan G.",
editor="Thiemann, Peter",
title="Visible Type Application",
booktitle="Programming Languages and Systems",
year="2016",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="229--254",
abstract="The Hindley-Milner (HM) type system automatically infers the types at which polymorphic functions are used. In HM, the inferred types are unambiguous, and every expression has a principal type. Type annotations make HM compatible with extensions where complete type inference is impossible, such as higher-rank polymorphism and type-level functions. However, programmers cannot use annotations to explicitly provide type arguments to polymorphic functions, as HM requires type instantiations to be inferred.",
isbn="978-3-662-49498-1"
}

@article{weirich-icfp17,
author = {Weirich, Stephanie and Voizard, Antoine and de Amorim, Pedro Henrique Azevedo and Eisenberg, Richard A.},
title = {A Specification for Dependent Types in Haskell},
year = {2017},
issue_date = {September 2017},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {1},
number = {ICFP},
url = {https://doi.org/10.1145/3110275},
doi = {10.1145/3110275},
abstract = { We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum
dependent types. Our semantics consists of two related languages. The first is a Curry-style
dependently-typed language with nontermination, irrelevant arguments, and equality
abstraction. The second, inspired by the Glasgow Haskell Compiler's core language
FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our
results---chiefly, type safety, along with theorems that relate these two languages---have
been formalized using the Coq proof assistant. Because our work is backwards compatible
with Haskell, our type safety proof holds in the presence of nonterminating computation.
However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda
or Idris, because of this nontermination, Haskell's term language does not correspond
to a consistent logic. },
journal = {Proc. ACM Program. Lang.},
month = aug,
articleno = {31},
numpages = {29},
keywords = {Dependent Types, Haskell}
}

@Article{type-classes-impl,
  Title                    = {Type Classes in Haskell},
  Author                   = {Hall, Cordelia V. and Hammond, Kevin and Peyton Jones, Simon L. and Wadler, Philip L.},
  Journal                  = {ACM Trans. Program. Lang. Syst.},
  Year                     = {1996},

  Month                    = mar,
  Number                   = {2},
  Volume                   = {18},

  Issue_date               = {March 1996},
  Keywords                 = {Haskell, functional programming, type classes, types},
  Publisher                = {ACM}
}

@InProceedings{linear-types-inference,
author="Matsuda, Kazutaka",
editor="M{\"u}ller, Peter",
title="Modular Inference of Linear Types for Multiplicity-Annotated Arrows",
booktitle="Programming Languages and Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="456--483",
abstract="Bernardy et al. [2018] proposed a linear type system {\$}{\$}{\backslash}lambda ^q{\_}{\backslash}rightarrow {\$}{\$}$\lambda${\textrightarrow}qas a core type system of Linear Haskell. In the system, linearity is represented by annotated arrow types {\$}{\$}A {\backslash}rightarrow {\_}m B{\$}{\$}A{\textrightarrow}mB, where m denotes the multiplicity of the argument. Thanks to this representation, existing non-linear code typechecks as it is, and newly written linear code can be used with existing non-linear code in many cases. However, little is known about the type inference of {\$}{\$}{\backslash}lambda ^q{\_}{\backslash}rightarrow {\$}{\$}$\lambda${\textrightarrow}q. Although the Linear Haskell implementation is equipped with type inference, its algorithm has not been formalized, and the implementation often fails to infer principal types, especially for higher-order functions. In this paper, based on OutsideIn(X) [Vytiniotis et al., 2011], we propose an inference system for a rank 1 qualified-typed variant of {\$}{\$}{\backslash}lambda ^q{\_}{\backslash}rightarrow {\$}{\$}$\lambda${\textrightarrow}q, which infers principal types. A technical challenge in this new setting is to deal with ambiguous types inferred by naive qualified typing. We address this ambiguity issue through quantifier elimination and demonstrate the effectiveness of the approach with examples.",
isbn="978-3-030-44914-8"
}

@InProceedings{hereditary-harrop,
  author = 	 {Dale A. Miller and Gopalan Nadathur and Andre Scedrov},
  title = 	 {Hereditary Harrop Formulas and Uniform Proof Systems},
  booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
  year =	 {1987},
  month =	 {June},
  pages =      {98--105},
  location =   {Ithaca, NY, USA},
  publisher =	 {IEEE Computer Society Press}
}

@thesis{hodas-thesis-lolli,
  author = {Joshua Seth Hodas},
  title = {Logic programming in intuitionistic linear logic: Theory, design, and implementation},
  year = {1994},
  url = {https://repository.upenn.edu/dissertations/AAI9427546}
}

@article{coherence,
author = {Bottu, Gert-Jan and Xie, Ningning and Marntirosian, Koar and Schrijvers, Tom},
title = {Coherence of Type Class Resolution},
year = {2019},
issue_date = {August 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {ICFP},
url = {https://doi.org/10.1145/3341695},
doi = {10.1145/3341695},
abstract = {Elaboration-based type class resolution, as found in languages like Haskell, Mercury
and PureScript, is generally nondeterministic: there can be multiple ways to satisfy
a wanted constraint in terms of global instances and locally given constraints. Coherence
is the key property that keeps this sane; it guarantees that, despite the nondeterminism,
programs still behave predictably. Even though elaboration-based resolution is generally
assumed coherent, as far as we know, there is no formal proof of this property in
the presence of sources of nondeterminism, like superclasses and flexible contexts.
This paper provides a formal proof to remedy the situation. The proof is non-trivial
because the semantics elaborates resolution into a target language where different
elaborations can be distinguished by contexts that do not have a source language counterpart.
Inspired by the notion of full abstraction, we present a two-step strategy that first
elaborates nondeterministically into an intermediate language that preserves contextual
equivalence, and then deterministically elaborates from there into the target language.
We use an approach based on logical relations to establish contextual equivalence
and thus coherence for the first step of elaboration, while the second step’s determinism
straightforwardly preserves this coherence property.},
journal = {Proc. ACM Program. Lang.},
month = jul,
articleno = {91},
numpages = {28},
keywords = {coherence, logical relations, type class resolution}
}

@article{resource-usage-analysis,
author = {Igarashi, Atsushi and Kobayashi, Naoki},
title = {Resource Usage Analysis},
year = {2005},
issue_date = {March 2005},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {27},
number = {2},
issn = {0164-0925},
url = {https://doi.org/10.1145/1057387.1057390},
doi = {10.1145/1057387.1057390},
abstract = {It is an important criterion of program correctness that a program accesses resources
in a valid manner. For example, a memory region that has been allocated should eventually
be deallocated, and after the deallocation, the region should no longer be accessed.
A file that has been opened should be eventually closed. So far, most of the methods
to analyze this kind of property have been proposed in rather specific contexts (like
studies of memory management and verification of usage of lock primitives), and it
was not clear what the essence of those methods was or how methods proposed for individual
problems are related. To remedy this situation, we formalize a general problem of
analyzing resource usage as a resource usage analysis problem, and propose a type-based
method as a solution to the problem.},
journal = {ACM Trans. Program. Lang. Syst.},
month = mar,
pages = {264–313},
numpages = {50},
keywords = {type inference, Resource usage}
}

@article{linearity-and-pi-calculus,
author = {Kobayashi, Naoki and Pierce, Benjamin C. and Turner, David N.},
title = {Linearity and the Pi-Calculus},
year = {1999},
issue_date = {Sept. 1999},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {21},
number = {5},
issn = {0164-0925},
url = {https://doi.org/10.1145/330249.330251},
doi = {10.1145/330249.330251},
abstract = {The economy and flexibility of the pi-calculus make it an attractive object of theoretical
study and a clean basis for concurrent language design and implementation. However,
such generality has a cost: encoding higher-level features like functional computation
in pi-calculus throws away potentially useful information. We show how a linear type
system can be used to recover important static information about a process's behavior.
In particular, we can guarantee that two processes communicating over a linear channel
cannot interfere with other communicating processes. After developing standard results
such as soundness of typing, we focus on equivalences, adapting the standard notion
of barbed bisimulation to the linear setting and showing how reductions on linear
channels induce a  useful “partial confluence” of process behaviors. For an extended
example of the theory, we prove the validity of a tail-call optimization for higher-order
functions represented as processes.},
journal = {ACM Trans. Program. Lang. Syst.},
month = sep,
pages = {914–947},
numpages = {34},
keywords = {confluence, linear types, process calculi, concurrency, pi-calculus}
}

@article{kindly-bent,
author = {Radanne, Gabriel and Saffrich, Hannes and Thiemann, Peter},
title = {Kindly Bent to Free Us},
year = {2020},
issue_date = {August 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {ICFP},
url = {https://doi.org/10.1145/3408985},
doi = {10.1145/3408985},
abstract = {Systems programming often requires the manipulation of resources like file handles,
network connections, or dynamically allocated memory. Programmers need to follow certain
protocols to handle these resources correctly. Violating these protocols causes bugs
ranging from type mismatches over data races to use-after-free errors and memory leaks.
These bugs often lead to security vulnerabilities. While statically typed programming
languages guarantee type soundness and memory safety by design, most of them do not
address issues arising from improper handling of resources. An important step towards
handling resources is the adoption of linear and affine types that enforce single-threaded
resource usage. However, the few languages supporting such types require heavy type
annotations. We present Affe, an extension of ML that manages linearity and affinity
properties using kinds and constrained types. In addition Affe supports the exclusive
and shared borrowing of affine resources, inspired by features of Rust. Moreover,
Affe retains the defining features of the ML family: it is an impure, strict, functional
expression language with complete principal type inference and type abstraction. does
not require any linearity annotations in expressions and supports common functional
programming idioms.},
journal = {Proc. ACM Program. Lang.},
month = aug,
articleno = {103},
numpages = {29},
keywords = {Ownership, Linear types, Type inference, Functional programming}
}

@article{abel_unified_2020,
	author = {Andreas Abel and Jean-Philippe Bernardy},
	title = {A unified view of modalities in type systems},
	journal = {Proceedings of the ACM on Programming Languages},
	volume = {4},
	number = {ICFP},
	year = {2020},
	publisher = {ACM}
},


@inproceedings{DBLP:conf/popl/CraryWM99,
  author    = {Karl Crary and
               David Walker and
               J. Gregory Morrisett},
  editor    = {Andrew W. Appel and
               Alex Aiken},
  title     = {Typed Memory Management in a Calculus of Capabilities},
  booktitle = {{POPL} '99, Proceedings of the 26th {ACM} {SIGPLAN-SIGACT} Symposium
               on Principles of Programming Languages, San Antonio, TX, USA, January
               20-22, 1999},
  pages     = {262--275},
  publisher = {{ACM}},
  year      = {1999},
  url       = {https://doi.org/10.1145/292540.292564},
  doi       = {10.1145/292540.292564},
  timestamp = {Tue, 06 Nov 2018 11:07:43 +0100},
  biburl    = {https://dblp.org/rec/conf/popl/CraryWM99.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/esop/SmithWM00,
  author    = {Frederick Smith and
               David Walker and
               J. Gregory Morrisett},
  editor    = {Gert Smolka},
  title     = {Alias Types},
  booktitle = {Programming Languages and Systems, 9th European Symposium on Programming,
               {ESOP} 2000, Held as Part of the European Joint Conferences on the
               Theory and Practice of Software, {ETAPS} 2000, Berlin, Germany, March
               25 - April 2, 2000, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1782},
  pages     = {366--381},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/3-540-46425-5_24},
  doi       = {10.1007/3-540-46425-5_24},
  timestamp = {Tue, 14 May 2019 10:00:41 +0200},
  biburl    = {https://dblp.org/rec/conf/esop/SmithWM00.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tic/WalkerM00,
  author    = {David Walker and
               J. Gregory Morrisett},
  editor    = {Robert Harper},
  title     = {Alias Types for Recursive Data Structures},
  booktitle = {Types in Compilation, Third International Workshop, {TIC} 2000, Montreal,
               Canada, September 21, 2000, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {2071},
  pages     = {177--206},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/3-540-45332-6_7},
  doi       = {10.1007/3-540-45332-6_7},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/conf/tic/WalkerM00.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/toplas/TerauchiA08,
  author    = {Tachio Terauchi and
               Alex Aiken},
  title     = {Witnessing side effects},
  journal   = {{ACM} Trans. Program. Lang. Syst.},
  volume    = {30},
  number    = {3},
  pages     = {15:1--15:42},
  year      = {2008},
  url       = {https://doi.org/10.1145/1353445.1353449},
  doi       = {10.1145/1353445.1353449},
  timestamp = {Tue, 06 Nov 2018 12:51:29 +0100},
  biburl    = {https://dblp.org/rec/journals/toplas/TerauchiA08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/sas/YasuokaT09,
  author    = {Hirotoshi Yasuoka and
               Tachio Terauchi},
  editor    = {Jens Palsberg and
               Zhendong Su},
  title     = {Polymorphic Fractional Capabilities},
  booktitle = {Static Analysis, 16th International Symposium, {SAS} 2009, Los Angeles,
               CA, USA, August 9-11, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5673},
  pages     = {36--51},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-03237-0_5},
  doi       = {10.1007/978-3-642-03237-0_5},
  timestamp = {Thu, 02 Dec 2021 11:46:17 +0100},
  biburl    = {https://dblp.org/rec/conf/sas/YasuokaT09.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/esop/FluetMA06,
  author    = {Matthew Fluet and
               Greg Morrisett and
               Amal J. Ahmed},
  editor    = {Peter Sestoft},
  title     = {Linear Regions Are All You Need},
  booktitle = {Programming Languages and Systems, 15th European Symposium on Programming,
               {ESOP} 2006, Held as Part of the Joint European Conferences on Theory
               and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28,
               2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3924},
  pages     = {7--21},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11693024_2},
  doi       = {10.1007/11693024_2},
  timestamp = {Sun, 02 Jun 2019 21:23:56 +0200},
  biburl    = {https://dblp.org/rec/conf/esop/FluetMA06.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@inproceedings{DBLP:conf/pldi/DeLineF01,
  author    = {Robert DeLine and
               Manuel F{\"{a}}hndrich},
  editor    = {Michael Burke and
               Mary Lou Soffa},
  title     = {Enforcing High-Level Protocols in Low-Level Software},
  booktitle = {Proceedings of the 2001 {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation (PLDI), Snowbird, Utah, USA, June
               20-22, 2001},
  pages     = {59--69},
  publisher = {{ACM}},
  year      = {2001},
  url       = {https://doi.org/10.1145/378795.378811},
  doi       = {10.1145/378795.378811},
  timestamp = {Wed, 07 Jul 2021 17:30:34 +0200},
  biburl    = {https://dblp.org/rec/conf/pldi/DeLineF01.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/pldi/FahndrichD02,
  author    = {Manuel F{\"{a}}hndrich and
               Robert DeLine},
  editor    = {Jens Knoop and
               Laurie J. Hendren},
  title     = {Adoption and Focus: Practical Linear Types for Imperative Programming},
  booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation (PLDI), Berlin, Germany, June 17-19,
               2002},
  pages     = {13--24},
  publisher = {{ACM}},
  year      = {2002},
  url       = {https://doi.org/10.1145/512529.512532},
  doi       = {10.1145/512529.512532},
  timestamp = {Wed, 07 Jul 2021 17:30:34 +0200},
  biburl    = {https://dblp.org/rec/conf/pldi/FahndrichD02.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{subexponentials,
author="Danos, Vincent
and Joinet, Jean -Baptiste
and Schellinx, Harold",
editor="Gottlob, Georg
and Leitsch, Alexander
and Mundici, Daniele",
title="The structure of exponentials: Uncovering the dynamics of linear logic proofs",
booktitle="Computational Logic and Proof Theory",
year="1993",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="159--171",
abstract="We construct the exponential graph of a proof $\pi$ in (second order) linear logic, an artefact displaying the interdependencies of exponentials in $\pi$. Within this graph superfluous exponentials are defined, the removal of which is shown to yield a correct proof $\pi$▹ with essentially the same set of reductions.",
isbn="978-3-540-47943-7"
}

@codefragment{prototype,
title={Prototype implementation of linear constraints in GHC},
author={Kiss, Csongor and Spiwack, Arnaud and Bernardy, Jean-Philippe and Wu, Nicolas and Eisenberg, Richard A.},
year="2022",
swhid={swh:1:rev:f6fc5ba23770b42d1d6020e177787757b16a9ea0;origin=https://github.com/kcsongor/ghc;visit=swh:1:snp:aa61d803eaec9eb4425e3eb8ed2b0fbbd60633cc},
}

@article{extended-version,
  author    = {Arnaud Spiwack and
               Csongor Kiss and
               Jean{-}Philippe Bernardy and
               Nicolas Wu and
               Richard A. Eisenberg},
  title     = {Linear Constraints},
  journal   = {CoRR},
  volume    = {abs/2103.06127},
  year      = {2021},
  url       = {https://arxiv.org/abs/2103.06127},
  eprinttype = {arXiv},
  eprint    = {2103.06127},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2103-06127.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}