ref.bib

@article{Hindley1969_PrincipalTypeScheme,
  issn      = {00029947},
  url       = {http://www.jstor.org/stable/1995158},
  author    = {R. Hindley},
  journal   = {Transactions of the American Mathematical Society},
  pages     = {29--60},
  publisher = {American Mathematical Society},
  doi       = {10.2307/1995158},
  title     = {The Principal Type-Scheme of an Object in Combinatory Logic},
  volume    = {146},
  year      = {1969}
}

@article{Milner1978_TypePolymorphism,
  title    = {A theory of type polymorphism in programming},
  journal  = {Journal of Computer and System Sciences},
  volume   = {17},
  number   = {3},
  pages    = {348-375},
  year     = {1978},
  issn     = {0022-0000},
  doi      = {https://doi.org/10.1016/0022-0000(78)90014-4},
  url      = {https://www.sciencedirect.com/science/article/pii/0022000078900144},
  author   = {Robin Milner},
  abstract = {The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types, entails defining procedures which work well on objects of a wide variety. We present a formal type discipline for such polymorphic procedures in the context of a simple programming language, and a compile time type-checking algorithm W which enforces the discipline. A Semantic Soundness Theorem (based on a formal semantics for the language) states that well-type programs cannot “go wrong” and a Syntactic Soundness Theorem states that if W accepts a program then it is well-typed. We also discuss extending these results to richer languages; a type-checking algorithm based on W is in fact already implemented and working, for the metalanguage ML in the Edinburgh LCF system.}
}

@inproceedings{DamasMilner1982_TypeSchemes,
  author    = {Damas, Luis and Milner, Robin},
  title     = {Principal type-schemes for functional programs},
  year      = {1982},
  isbn      = {0897910656},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  doi       = {10.1145/582153.582176},
  booktitle = {Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages     = {207–212},
  numpages  = {6},
  location  = {Albuquerque, New Mexico},
  series    = {POPL '82}
}

@article{Damas1984_TypeAssignment,
  title     = {Type assignment in programming languages},
  author    = {Damas, Luis},
  journal   = {KB thesis scanning project 2015},
  year      = {1984},
  publisher = {The University of Edinburgh}
}

@inproceedings{Clement1986_MiniML,
  author    = {Cl\'{e}ment, Dominique and Despeyroux, Thierry and Kahn, Gilles and Despeyroux, Jo\"{e}lle},
  title     = {A simple applicative language: mini-ML},
  year      = {1986},
  isbn      = {0897912004},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  doi       = {10.1145/319838.319847},
  booktitle = {Proceedings of the 1986 ACM Conference on LISP and Functional Programming},
  pages     = {13–27},
  numpages  = {15},
  location  = {Cambridge, Massachusetts, USA},
  series    = {LFP '86}
}

@techreport{Remy1992_SortedEqTheoryTypes,
  title       = {{Extension of ML type system with a sorted equation theory on types}},
  author      = {R{\'e}my, Didier},
  url         = {https://inria.hal.science/inria-00077006},
  type        = {Research Report},
  number      = {RR-1766},
  institution = {{INRIA}},
  year        = {1992}
}

@misc{Kiselyov2022_OCamplTypeChecker,
  author = {Oleg Kiselyov},
  title  = {{How OCaml type checker works — or what polymorphism and garbage collection have in common}},
  url    = {https://okmij.org/ftp/ML/generalization.html},
  year   = {2022},
  month  = {01},
  day    = {9}
}

@inproceedings{Mairson1989_MLTypabilityExponential,
  author    = {Mairson, Harry G.},
  title     = {Deciding ML typability is complete for deterministic exponential time},
  year      = {1989},
  isbn      = {0897913434},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/96709.96748},
  doi       = {10.1145/96709.96748},
  booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  pages     = {382–401},
  numpages  = {20},
  location  = {San Francisco, California, USA},
  series    = {POPL '90}
}

@article{Simon2002_SecretsGHC,
  author  = {Peyton Jones, Simon and Marlow, Simon},
  title   = {{Secrets of the Glasgow Haskell Compiler inliner}},
  year    = {2002},
  month   = {7},
  url     = {https://www.microsoft.com/en-us/research/publication/secrets-of-the-glasgow-haskell-compiler-inliner/},
  pages   = {393-434},
  journal = {Journal of Functional Programming},
  volume  = {12}
}

@inproceedings{Foil,
  author    = {Maclaurin, Dougal and Radul, Alexey and Paszke, Adam},
  title     = {The Foil: Capture-Avoiding Substitution With No Sharp Edges},
  year      = {2023},
  isbn      = {9781450398312},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  doi       = {10.1145/3587216.3587224},
  abstract  = {Correctly manipulating program terms in a compiler is surprisingly difficult because of the need to avoid name capture. The rapier from Peyton Jones and Marlow [9] is a cutting-edge technique for fast, stateless capture-avoiding substitution for expressions represented with explicit names. It is, however, a sharp tool—its invariants are tricky and need to be maintained throughout the whole compiler that uses it. We describe the foil, an elaboration of the rapier that uses Haskell’s type system to enforce the rapier’s invariants statically, preventing a class of hard-to-find bugs, but without adding any run-time overheads.},
  booktitle = {Proceedings of the 34th Symposium on Implementation and Application of Functional Languages},
  articleno = {8},
  numpages  = {10},
  location  = {Copenhagen, Denmark},
  series    = {IFL '22}
}

@inproceedings{FreeFoil,
  author    = {Kudasov, Nikolai and Shakirova, Renata and Shalagin, Egor and Tyulebaeva, Karina},
  booktitle = {2024 4th International Conference on Code Quality (ICCQ)},
  title     = {Free Foil: Generating Efficient and Scope-Safe Abstract Syntax},
  year      = {2024},
  volume    = {},
  number    = {},
  pages     = {1-16},
  keywords  = {Codes;Prototypes;Syntactics;Benchmark testing;Generators;Encoding;Safety;abstract syntax;second-order;capture-avoiding substitution;free monads},
  doi       = {10.1109/ICCQ60895.2024.10576867}
}

@inproceedings{BNFC,
  author    = {Forsberg, Markus and Ranta, Aarne},
  title     = {{BNF converter}},
  year      = {2004},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  doi       = {10.1145/1017472.1017475},
  abstract  = {We will demonstrate BNFC (the BNF Converter) [7, 6], a multi-lingual compiler tool. BNFC takes as its input a grammar written in LBNF (Labelled BNF) notation, and generates a compiler front-end (an abstract syntax, a lexer, and a parser). Furthermore, it generates a case skeleton usable as the starting point of back-end construction, a pretty printer, a test bench, and a LaTeX document usable as language specification. The program components can be generated in Haskell, Java, C and C++ and their standard parser and lexer tools. BNFC itself was written in Haskell.The methodology used for the generated front-end is based on Appel's books on compiler construction [3, 1, 2]. BNFC has been used as a teaching tool in compiler construction courses at Chalmers. It has also been applied to research-related programming language development, and in an industrial application producing a compiler for a telecommunications protocol description language [4].BNFC is freely available under the GPL license at its website and in the testing distribution of Debian Linux.},
  booktitle = {Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell},
  pages     = {94–95},
  numpages  = {2},
  keywords  = {pretty printer, parser generator, grammar, document automation, compiler construction, abstract syntax, BNF},
  location  = {Snowbird, Utah, USA},
  series    = {Haskell '04}
}

@inproceedings{SheardPeytonJones2002_TH,
  title     = {Template meta-programming for Haskell},
  author    = {Sheard, Tim and Jones, Simon Peyton},
  booktitle = {Proceedings of the 2002 ACM SIGPLAN workshop on Haskell},
  publisher = {{ACM}},
  doi       = {10.1145/581690.581691},
  pages     = {1--16},
  year      = {2002}
}

@incollection{BackusNaurForm2003,
  title     = {Backus-naur form (bnf)},
  author    = {McCracken, Daniel D and Reilly, Edwin D},
  booktitle = {Encyclopedia of Computer Science},
  pages     = {129--131},
  year      = {2003}
}

@misc{haskell_happy,
  author       = {{Haskell Community}},
  title        = {Happy - The Parser Generator for Haskell},
  year         = {2024},
  howpublished = {\url{https://github.com/haskell/happy}}
}

@misc{haskell_alex,
  author       = {{Haskell Community}},
  title        = {Alex - A Lexical Analyser Generator for Haskell},
  year         = {2024},
  howpublished = {\url{https://github.com/haskell/alex}}
}

@inproceedings{deBruijn1972,
  title        = {{Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem}},
  author       = {De Bruijn, Nicolaas Govert},
  booktitle    = {Indagationes mathematicae (proceedings)},
  volume       = {75},
  number       = {5},
  pages        = {381--392},
  year         = {1972},
  organization = {Elsevier},
  doi          = {https://doi.org/10.1016/1385-7258(72)90034-0}
}

@article{BirdPaterson1999_BruijnNested,
  title   = {de Bruijn notation as a nested datatype},
  volume  = {9},
  doi     = {10.1017/S0956796899003366},
  number  = {1},
  journal = {Journal of Functional Programming},
  author  = {Bird, Richard S. and Paterson, Ross},
  year    = {1999},
  pages   = {77–91}
}

@inproceedings{Bird1998_NestedDatatypes,
  author  = {Bird, Richard and Meertens, Lambert},
  year    = {1998},
  month   = {06},
  pages   = {52-67},
  title   = {Nested Datatypes.},
  volume  = {1422},
  isbn    = {978-3-540-64591-7},
  journal = {Lecture Notes in Computer Science},
  doi     = {10.1007/BFb0054285}
}

@article{PaszkeDex_2021,
  author  = {Paszke, Adam and Johnson, Daniel D. and Duvenaud, David and Vytiniotis, Dimitrios and Radul, Alexey and Johnson, Matthew J. and Ragan-Kelley, Jonathan and Maclaurin, Dougal},
  doi     = {10.1145/3473593},
  journal = {Proceedings of the ACM on Programming Languages},
  month   = aug,
  title   = {Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array Programming},
  volume  = {5},
  year    = {2021}
}

@inproceedings{Traytel2011_HMCoerciveSubtyping,
  author    = {Traytel, Dmitriy
               and Berghofer, Stefan
               and Nipkow, Tobias},
  editor    = {Yang, Hongseok},
  title     = {Extending Hindley-Milner Type Inference with Coercive Structural Subtyping},
  booktitle = {Programming Languages and Systems},
  year      = {2011},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {89--104},
  abstract  = {We investigate how to add coercive structural subtyping to a type system for simply-typed lambda calculus with Hindley-Milner polymorphism. Coercions allow to convert between different types, and their automatic insertion can greatly increase readability of terms. We present a type inference algorithm that, given a term without type information, computes a type assignment and determines at which positions in the term coercions have to be inserted to make it type-correct according to the standard Hindley-Milner system (without any subtypes). The algorithm is sound and, if the subtype relation on base types is a disjoint union of lattices, also complete. The algorithm has been implemented in the proof assistant Isabelle.},
  isbn      = {978-3-642-25318-8}
}

@article{Robinson1965,
  author     = {Robinson, J. A.},
  title      = {A Machine-Oriented Logic Based on the Resolution Principle},
  year       = {1965},
  issue_date = {Jan. 1965},
  publisher  = {Association for Computing Machinery},
  address    = {New York, NY, USA},
  volume     = {12},
  number     = {1},
  issn       = {0004-5411},
  doi        = {10.1145/321250.321253},
  journal    = {J. ACM},
  month      = jan,
  pages      = {23–41},
  numpages   = {19}
}

@software{free-foil,
  author    = {Nikolai Kudasov and
               Egor Shalagin and
               Renata Shakirova},
  title     = {{fizruk/free-foil}},
  month     = oct,
  year      = 2024,
  publisher = {Zenodo},
  version   = {v0.2.0},
  doi       = {10.5281/zenodo.13997857}
}

@article{lee1998proofs,
  title     = {Proofs about a folklore let-polymorphic type inference algorithm},
  author    = {Lee, Oukseh and Yi, Kwangkeun},
  journal   = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume    = {20},
  number    = {4},
  pages     = {707--723},
  year      = {1998},
  publisher = {ACM New York, NY, USA}
}

@article{Heeren2002_GeneralizingHM,
  title     = {Generalizing Hindley-Milner type inference algorithms},
  author    = {Heeren, BJ and Hage, Jurriaan and Swierstra, S Doaitse and others},
  year      = {2002},
  publisher = {Utrecht University: Information and Computing Sciences}
}

@article{Swierstra2008_a_la_carte,
  title     = {Data types \`a la carte},
  volume    = {18},
  doi       = {10.1017/S0956796808006758},
  number    = {4},
  journal   = {Journal of Functional Programming},
  publisher = {Cambridge University Press},
  author    = {Swierstra, Wouter},
  year      = {2008},
  pages     = {423–436}
}