@book{noauthor_advanced_2005,
	title = {Advanced {Topics} in {Types} and {Programming} {Languages}},
	editor = {, Benjamin C. Pierce},
	year = {2005},
	file = {Advanced Topics in Types and Programming Languages.pdf:/home/micha/Zotero/storage/GZTFPV8C/Advanced Topics in Types and Programming Languages.pdf:application/pdf},
}

@book{noauthor_type_nodate,
	edition = {Working draft of January 15, 2000},
	title = {Type {Systems} for {Programming} {Languages}},
	author = {, Benjamin C. Pierce},
	file = {Type Systems for Programming Languages.pdf:/home/micha/Zotero/storage/DMRL4537/Type Systems for Programming Languages.pdf:application/pdf},
}

@article{christiansen_bidirectional_2013,
	title = {Bidirectional {Typing} {Rules}: {A} {Tutorial}},
	language = {en},
	author = {Christiansen, David Raymond},
	year = {2013},
	file = {bidirectional.pdf:/home/micha/papers/bidirectional.pdf:application/pdf},
}

@inproceedings{sippel_process_2023,
	address = {Koblenz Germany},
	title = {Process {Composition} with {Typed} {Unix} {Pipes}},
	isbn = {9798400704048},
	url = {https://dl.acm.org/doi/10.1145/3623759.3624546},
	doi = {10.1145/3623759.3624546},
	language = {en},
	urldate = {2024-07-23},
	booktitle = {Proceedings of the 12th {Workshop} on {Programming} {Languages} and {Operating} {Systems}},
	publisher = {ACM},
	author = {Sippel, Michael and Schirmeier, Horst},
	month = oct,
	year = {2023},
	pages = {34--40},
	file = {Sippel and Schirmeier - 2023 - Process Composition with Typed Unix Pipes.pdf:/home/micha/Zotero/storage/FB3SUV46/Sippel and Schirmeier - 2023 - Process Composition with Typed Unix Pipes.pdf:application/pdf},
}

@article{bohm_automatic_1984,
	title = {Automatic {Synthesis} of {Typed} Λ-{Progras} on {Term}-{Algebras}},
	abstract = {The notion of iteratively defined functions from and to heterogeneous term algebras is introduced as the solution of a finite set of equations of a special shape. Such a notion has remarkable consequences: (1) Choosing the second-order typed lambdacalculus (A for short) as a programming language enables one to represent algebra elements and iterative functions by automatic uniform synthesis paradigms, using neither conditional nor recursive constructs. (2) A completeness theorem for A-terms with type of degree at most two and a companion corollary for A-programs have been proved. (3) A new congruence relation for the last-mentioned A-terms which is stronger than A-convertibility is introduced and proved to have the meaning of a A-program equivalence. Moreover, an extension of the paradigms to the synthesis of functions of higher complexity is considered and exemplified. All the concepts are explained and motivated by examples over integers, list- and tree-structures.},
	language = {en},
	author = {Bohm, Corrado and Berarducci, Alessandro},
	month = may,
	year = {1984},
	file = {Bohm and Berarducci - AUTOMATIC SYNTHESIS OF TYPED A-PROGRAMS ON. TERM A.pdf:/home/micha/Zotero/storage/DVQEVUM3/Bohm and Berarducci - AUTOMATIC SYNTHESIS OF TYPED A-PROGRAMS ON. TERM A.pdf:application/pdf},
}

@article{cardelli_extension_1991,
	title = {An extension of system {F} with subtyping},
	abstract = {System F is a well-known typed λ-calculus with polymorphic types, which provides a basis for polymorphic programming languages. We study an extension of F, called F{\textless}: (pronounced ef-sub) that combines parametric polymorphism with subtyping.},
	language = {en},
	author = {Cardelli, Luca and Martini, Simone and Mitchell, John C and Scedrov, Andre},
	month = dec,
	year = {1991},
	file = {Cardelli et al. - An extension of system F with subtyping.pdf:/home/micha/Zotero/storage/YAUSALAD/Cardelli et al. - An extension of system F with subtyping.pdf:application/pdf},
}

@book{pierce_types_2002,
	address = {Cambridge, Mass},
	title = {Types and programming languages},
	isbn = {978-0-262-16209-8},
	language = {en},
	publisher = {MIT Press},
	author = {Pierce, Benjamin C.},
	year = {2002},
	keywords = {Programming languages (Electronic computers)},
	file = {Pierce - 2002 - Types and programming languages.pdf:/home/micha/Zotero/storage/WLKW9G4T/Pierce - 2002 - Types and programming languages.pdf:application/pdf},
}

@article{glew_type_1999,
	title = {Type {Dispatch} for {Named} {Hierarchical} {Types}},
	abstract = {Type dispatch constructs are an important feature of many programming languages. Scheme has predicates for testing the runtime type of a value. Java has a class cast expression and a try statement for switching on an exception’s class. Crucial to these mechanisms, in typed languages, is type refinement: The static type system will use type dispatch to refine types in successful dispatch branches. Existing work in functional languages has addressed certain kinds of type dispatch, namely, intensional type analysis. However, this work does not extend to languages with subtyping nor to named types.},
	language = {en},
	author = {Glew, Neal},
	month = apr,
	year = {1999},
	file = {Glew - Type Dispatch for Named Hierarchical Types.pdf:/home/micha/Zotero/storage/RNJGLK6H/Glew - Type Dispatch for Named Hierarchical Types.pdf:application/pdf},
}

@article{fluet_phantom_nodate,
	title = {Phantom {Types} and {Subtyping}},
	abstract = {We investigate a technique from the literature, called the phantom-types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in Standard ML, can be used to enforce the subtyping relation, at least for first-order values. We show that this technique can be used to encode any finite subtyping hierarchy (including hierarchies arising from multiple interface inheritance). We formally demonstrate the suitability of the phantom-types technique for capturing first-order subtyping by exhibiting a type-preserving translation from a simple calculus with bounded polymorphism to a calculus embodying the type system of SML.},
	language = {en},
	author = {Fluet, Matthew and Pucella, Riccardo},
	file = {Fluet and Pucella - Phantom Types and Subtyping.pdf:/home/micha/Zotero/storage/ADMMFHIF/Fluet and Pucella - Phantom Types and Subtyping.pdf:application/pdf},
}

@article{cardelli_abstract_1990,
	title = {Abstract types and the dot notation},
	language = {en},
	author = {Cardelli, Luca and Leroy, Xavier},
	month = mar,
	year = {1990},
	file = {Cardelli and Leroy - Abstract types and the dot notation.pdf:/home/micha/Zotero/storage/AASDBL4Z/Cardelli and Leroy - Abstract types and the dot notation.pdf:application/pdf},
}

@article{fortune_expressiveness_1983,
	title = {The {Expressiveness} of {Simple} and {Second}-{Order} {Type} {Structures}},
	volume = {30},
	issn = {0004-5411, 1557-735X},
	url = {https://dl.acm.org/doi/10.1145/322358.322370},
	doi = {10.1145/322358.322370},
	abstract = {Typed lambda (?`-) calculi provtde convement mathematical settings in which to investigate the effects of type structure on the function definmon mechamsm m programming languages. Lambda expressaons mtm{\textasciitilde}c programs that do not use while loops or carcular function definitions. Two typed ?`-calculi are investigated, the sunply typed ?`-calculus, whose types are similar to Pascal types, and the second-order typed ?,-calculus, which has a type abstractaon mechamsm simdar to that of modern data abstraction languages such as ALPHARD. Two related questions are considered for each calculus: (1) What functaons are definable m the calculus? and (2) How difficult is the proof that all expressions in the calculus are normahzable 0.e., that all computaUons termmate)* The simply typed calculus only defines elementary functtons. Normahzation for this calculus {\textasciitilde}s provable using commonplace forms of reasoning formalazable m Peano arithmetic The second-order calculus defines a huge hierarchy of funcuons going far beyond Ackermann's function These funcuons are so rapidly increasing that Peano arithmetic cannot prove that they are total In fact, normalizataon for the second-order calculus cannot be proved even m second-order Peano artthmetic, nor m Peano anthmettc augmented by all true statements Also d{\textasciitilde}scussed are the lmphcataons of the present ?`-calculus results for the programming languages PASCAL, ALPHARD, RUSSELL, and MODEL.},
	language = {en},
	number = {1},
	urldate = {2024-07-29},
	journal = {Journal of the ACM},
	author = {Fortune, Steven and Leivant, Daniel and O'Donnell, Michael},
	month = jan,
	year = {1983},
	pages = {151--185},
	file = {Fortune et al. - 1983 - The Expressiveness of Simple and Second-Order Type.pdf:/home/micha/Zotero/storage/QPRGAGLQ/Fortune et al. - 1983 - The Expressiveness of Simple and Second-Order Type.pdf:application/pdf},
}

@incollection{goos_towards_1974,
	address = {Berlin, Heidelberg},
	title = {Towards a theory of type structure},
	volume = {19},
	isbn = {978-3-540-06859-4 978-3-540-37819-8},
	url = {http://link.springer.com/10.1007/3-540-06859-7_148},
	language = {en},
	urldate = {2024-07-29},
	booktitle = {Programming {Symposium}},
	publisher = {Springer Berlin Heidelberg},
	author = {Reynolds, John C.},
	editor = {Goos, G. and Hartmanis, J. and Brinch Hansen, P. and Gries, D. and Moler, C. and Seegmüller, G. and Wirth, N. and Robinet, B.},
	year = {1974},
	doi = {10.1007/3-540-06859-7_148},
	note = {Series Title: Lecture Notes in Computer Science},
	pages = {408--425},
	file = {Reynolds - 1974 - Towards a theory of type structure.pdf:/home/micha/Zotero/storage/TBXSMB4V/Reynolds - 1974 - Towards a theory of type structure.pdf:application/pdf},
}

@inproceedings{crary_flexible_1999,
	address = {Paris France},
	title = {Flexible type analysis},
	isbn = {978-1-58113-111-6},
	url = {https://dl.acm.org/doi/10.1145/317636.317906},
	doi = {10.1145/317636.317906},
	language = {en},
	urldate = {2024-07-29},
	booktitle = {Proceedings of the fourth {ACM} {SIGPLAN} international conference on {Functional} programming},
	publisher = {ACM},
	author = {Crary, Karl and Weirich, Stephanie},
	month = sep,
	year = {1999},
	pages = {233--248},
	file = {Full Text:/home/micha/Zotero/storage/KJJG9TI6/Crary and Weirich - 1999 - Flexible type analysis.pdf:application/pdf},
}

@article{wilson_pointer_1991,
	title = {Pointer swizzling at page fault time: efficiently supporting huge address spaces on standard hardware},
	volume = {19},
	issn = {0163-5964},
	shorttitle = {Pointer swizzling at page fault time},
	url = {https://dl.acm.org/doi/10.1145/122576.122577},
	doi = {10.1145/122576.122577},
	abstract = {We describe a scheme for supporting huge address spaces without the need for long addresses implemented in hardware. Pointers are translated ("swizzled") from a long format to a shorter format (directly supported by normal hardware) at page fault time. No extra hardware is required beyond that normally used by virtual memory systems, and no continual software cost is incurred by presence checks or indirection of pointers.},
	language = {en},
	number = {4},
	urldate = {2024-08-23},
	journal = {ACM SIGARCH Computer Architecture News},
	author = {Wilson, Paul R.},
	month = jul,
	year = {1991},
	pages = {6--13},
	file = {Wilson - 1991 - Pointer swizzling at page fault time efficiently .pdf:/home/micha/Zotero/storage/KW979W6S/Wilson - 1991 - Pointer swizzling at page fault time efficiently .pdf:application/pdf},
}

@incollection{goos_coercive_1997,
	address = {Berlin, Heidelberg},
	title = {Coercive subtyping in type theory},
	volume = {1258},
	isbn = {978-3-540-63172-9 978-3-540-69201-0},
	url = {http://link.springer.com/10.1007/3-540-63172-0_45},
	abstract = {We propose and study coercive subtyping, a formal extension with subtyping of dependent type theories such as Martin-Lof's type theory NPS90] and the type theory UTT Luo94]. In this approach, subtyping with speci ed implicit coercions is treated as a feature at the level of the logical framework; in particular, subsumption and coercion are combined in such a way that the meaning of an object being in a supertype is given by coercive de nition rules for the de nitional equality. It is shown that this provides a conceptually simple and uniform framework to understand subtyping and coercion relations in type theories with sophisticated type structures such as inductive types and universes. The use of coercive subtyping in formal development and in reasoning about subsets of objects is discussed in the context of computerassisted formal reasoning.},
	language = {en},
	urldate = {2024-09-08},
	booktitle = {Computer {Science} {Logic}},
	publisher = {Springer Berlin Heidelberg},
	author = {Luo, Zhaohui},
	editor = {Goos, Gerhard and Hartmanis, Juris and Leeuwen, Jan and Dalen, Dirk and Bezem, Marc},
	year = {1997},
	doi = {10.1007/3-540-63172-0_45},
	note = {Series Title: Lecture Notes in Computer Science},
	pages = {275--296},
	file = {Luo - 1997 - Coercive subtyping in type theory.pdf:/home/micha/Zotero/storage/2N7457L7/Luo - 1997 - Coercive subtyping in type theory.pdf:application/pdf},
}

@article{luo_coercive_2013,
	title = {Coercive subtyping: {Theory} and implementation},
	volume = {223},
	copyright = {https://www.elsevier.com/tdm/userlicense/1.0/},
	issn = {08905401},
	shorttitle = {Coercive subtyping},
	url = {https://linkinghub.elsevier.com/retrieve/pii/S0890540112001757},
	doi = {10.1016/j.ic.2012.10.020},
	abstract = {Coercive subtyping is a useful and powerful framework of subtyping for type theories. The key idea of coercive subtyping is subtyping as abbreviation. In this paper, we give a new and adequate formulation of T [C], the system that extends a type theory T with coercive subtyping based on a set C of basic subtyping judgements, and show that coercive subtyping is a conservative extension and, in a more general sense, a definitional extension. We introduce an intermediate system, the star-calculus T [C]∗, in which the positions that require coercion insertions are marked, and show that T [C]∗ is a conservative extension of T and that T [C]∗ is equivalent to T [C]. This makes clear what we mean by coercive subtyping being a conservative extension, on the one hand, and amends a technical problem that has led to a gap in the earlier conservativity proof, on the other. We also compare coercive subtyping with the ‘ordinary’ notion of subtyping – subsumptive subtyping, and show that the former is adequate for type theories with canonical objects while the latter is not. An improved implementation of coercive subtyping is done in the proof assistant Plastic.},
	language = {en},
	urldate = {2024-09-08},
	journal = {Information and Computation},
	author = {Luo, Z. and Soloviev, S. and Xue, T.},
	month = feb,
	year = {2013},
	pages = {18--42},
	file = {Luo et al. - 2013 - Coercive subtyping Theory and implementation.pdf:/home/micha/Zotero/storage/ZSCYFNK2/Luo et al. - 2013 - Coercive subtyping Theory and implementation.pdf:application/pdf},
}

@article{luo_transitivity_2004,
	title = {Transitivity in {Coercive} {Subtyping} ⋆},
	abstract = {Coercive subtyping is a general approach to abbreviation and subtyping in dependent type theories with inductive types. Coherence and admissibility of transitivity are important both for understanding of the framework and for its correct implementation. In this paper, we study the issue of transitivity in the context of subtyping for parameterised inductive types. In particular, we propose and study the notion of weak transitivity and show that, for a large class of parameterised inductive types, the natural subtyping rules are coherent and weak transitivity is admissible in an intensional type theory. A possible extension of type theory with certain extensional computation rules is also discussed for achieving admissibility of transitivity in general.},
	language = {en},
	author = {Luo, Zhaohui and Luo, Yong},
	year = {2004},
	file = {Luo and Luo - Transitivity in Coercive Subtyping ⋆.pdf:/home/micha/Zotero/storage/AGS2UM4S/Luo and Luo - Transitivity in Coercive Subtyping ⋆.pdf:application/pdf},
}

@article{luo_coherence_2004,
	title = {Coherence and {Transitivity} in {Coercive} {Subtyping}},
	abstract = {The aim of this thesis is to study coherence and transitivity in coercive subtyping. Among other things, coherence and transitivity are key aspects for a coercive subtyping system to be consistent and for it to be implemented in a correct way. The thesis consists of three major parts.},
	language = {en},
	author = {Luo, Yong},
	year = {2004},
	file = {Luo - Coherence and Transitivity in Coercive Subtyping.pdf:/home/micha/Zotero/storage/WYVDZWFA/Luo - Coherence and Transitivity in Coercive Subtyping.pdf:application/pdf},
}

@article{callaghan_coercive_2008,
	title = {Coercive {Subtyping} via {Mappings} of {Reduction} {Behaviour}},
	volume = {196},
	copyright = {https://www.elsevier.com/tdm/userlicense/1.0/},
	issn = {15710661},
	url = {https://linkinghub.elsevier.com/retrieve/pii/S1571066108000376},
	doi = {10.1016/j.entcs.2007.09.017},
	abstract = {This paper reports preliminary work on a novel approach to Coercive Subtyping that is based on relationships between reduction behaviour of source and target types in coerced terms. Coercive Subtyping is a superset of record-based subtyping, allowing so-called coercion functions to carry the subtyping. This allows many novel and powerful forms of subtyping and abbreviation, with applications including interfaces to theorem provers and programming with dependent type systems. However, the use of coercion functions introduces non-trivial overheads, and requires difficult proof of properties such as coherence in order to guarantee sensible results. These points restrict the practicality of coercive subtyping.},
	language = {en},
	urldate = {2024-09-08},
	journal = {Electronic Notes in Theoretical Computer Science},
	author = {Callaghan, Paul},
	month = jan,
	year = {2008},
	pages = {53--68},
	file = {Callaghan - 2008 - Coercive Subtyping via Mappings of Reduction Behav.pdf:/home/micha/Zotero/storage/66B6R9YL/Callaghan - 2008 - Coercive Subtyping via Mappings of Reduction Behav.pdf:application/pdf},
}

@article{luo_formal_2012,
	title = {Formal semantics in modern type theories with coercive subtyping},
	volume = {35},
	copyright = {http://www.springer.com/tdm},
	issn = {0165-0157, 1573-0549},
	url = {http://link.springer.com/10.1007/s10988-013-9126-4},
	doi = {10.1007/s10988-013-9126-4},
	abstract = {In the formal semantics based on modern type theories, common nouns are interpreted as types, rather than as predicates of entities as in Montague’s semantics. This brings about important advantages in linguistic interpretations but also leads to a limitation of expressive power because there are fewer operations on types as compared with those on predicates. The theory of coercive subtyping adequately extends the modern type theories and, as shown in this paper, plays a very useful role in making type theories more expressive for formal semantics. It not only gives a satisfactory solution to the basic problem of ‘multiple categorisation’ caused by interpreting common nouns as types, but provides a powerful formal framework to model interesting linguistic phenomena such as copredication, whose formal treatment has been found difficult in a Montagovian setting. In particular, we show how to formally introduce dot-types in a type theory with coercive subtyping and study some type-theoretic constructs that provide useful representational tools for reference transfers and multiple word meanings in formal lexical semantics.},
	language = {en},
	number = {6},
	urldate = {2024-09-08},
	journal = {Linguistics and Philosophy},
	author = {Luo, Zhaohui},
	month = nov,
	year = {2012},
	pages = {491--513},
	file = {Luo - 2012 - Formal semantics in modern type theories with coer.pdf:/home/micha/Zotero/storage/3GBMP8T4/Luo - 2012 - Formal semantics in modern type theories with coer.pdf:application/pdf},
}

@article{breitner_safe_2016,
	title = {Safe zero-cost coercions for {Haskell}},
	volume = {26},
	copyright = {https://www.cambridge.org/core/terms},
	issn = {0956-7968, 1469-7653},
	url = {https://www.cambridge.org/core/product/identifier/S0956796816000150/type/journal_article},
	doi = {10.1017/S0956796816000150},
	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.},
	language = {en},
	urldate = {2024-09-08},
	journal = {Journal of Functional Programming},
	author = {Breitner, Joachim and Eisenberg, Richard A. and Peyton Jones, Simon and Weirich, Stephanie},
	year = {2016},
	pages = {e15},
	file = {Breitner et al. - 2016 - Safe zero-cost coercions for Haskell.pdf:/home/micha/Zotero/storage/Y8QUMMBA/Breitner et al. - 2016 - Safe zero-cost coercions for Haskell.pdf:application/pdf},
}

@inproceedings{sulzmann_system_2007,
	address = {Nice Nice, France},
	title = {System {F} with type equality coercions},
	isbn = {978-1-59593-393-5},
	url = {https://dl.acm.org/doi/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.},
	language = {en},
	urldate = {2024-09-08},
	booktitle = {Proceedings of the 2007 {ACM} {SIGPLAN} international workshop on {Types} in languages design and implementation},
	publisher = {ACM},
	author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
	month = jan,
	year = {2007},
	pages = {53--66},
	file = {Sulzmann et al. - 2007 - System F with type equality coercions.pdf:/home/micha/Zotero/storage/NJATU92V/Sulzmann et al. - 2007 - System F with type equality coercions.pdf:application/pdf},
}

@inproceedings{weirich_system_2013,
	address = {Boston Massachusetts USA},
	title = {System {FC} with explicit kind equality},
	isbn = {978-1-4503-2326-0},
	url = {https://dl.acm.org/doi/10.1145/2500365.2500599},
	doi = {10.1145/2500365.2500599},
	abstract = {System FC, the core language of the Glasgow Haskell Compiler, is an explicitly-typed variant of System F with first-class type equality proofs called coercions. This extensible proof system forms the foundation for type system extensions such as type families (typelevel functions) and Generalized Algebraic Datatypes (GADTs). Such features, in conjunction with kind polymorphism and datatype promotion, support expressive compile-time reasoning.},
	language = {en},
	urldate = {2024-09-08},
	booktitle = {Proceedings of the 18th {ACM} {SIGPLAN} international conference on {Functional} programming},
	publisher = {ACM},
	author = {Weirich, Stephanie and Hsu, Justin and Eisenberg, Richard A.},
	month = sep,
	year = {2013},
	pages = {275--286},
	file = {Weirich et al. - 2013 - System FC with explicit kind equality.pdf:/home/micha/Zotero/storage/PM78RWRN/Weirich et al. - 2013 - System FC with explicit kind equality.pdf:application/pdf},
}

@article{marie-magdeleine_sous-typage_2009,
	title = {Sous-typage coercitif en présence de réductions non-standards dans un système aux types dépendants},
	language = {fr},
	author = {Marie-Magdeleine, Lionel},
	year = {2009},
	file = {Marie-Magdeleine - Sous-typage coercitif en présence de réductions no.pdf:/home/micha/Zotero/storage/WXATHUFU/Marie-Magdeleine - Sous-typage coercitif en présence de réductions no.pdf:application/pdf},
}

@article{breazu-tannen_inheritance_1991,
	title = {Inheritance as implicit coercion},
	volume = {93},
	issn = {08905401},
	url = {https://linkinghub.elsevier.com/retrieve/pii/0890540191900557},
	doi = {10.1016/0890-5401(91)90055-7},
	language = {en},
	number = {1},
	urldate = {2024-09-09},
	journal = {Information and Computation},
	author = {Breazu-Tannen, Val and Coquand, Thierry and Gunter, Carl A. and Scedrov, Andre},
	month = jul,
	year = {1991},
	pages = {172--221},
	file = {Breazu-Tannen et al. - 1991 - Inheritance as implicit coercion.pdf:/home/micha/Zotero/storage/43RB8XQM/Breazu-Tannen et al. - 1991 - Inheritance as implicit coercion.pdf:application/pdf},
}

@inproceedings{chen_coercive_2003,
	address = {New Orleans Louisiana USA},
	title = {Coercive subtyping for the calculus of constructions},
	isbn = {978-1-58113-628-9},
	url = {https://dl.acm.org/doi/10.1145/604131.604145},
	doi = {10.1145/604131.604145},
	language = {en},
	urldate = {2024-09-10},
	booktitle = {Proceedings of the 30th {ACM} {SIGPLAN}-{SIGACT} symposium on {Principles} of programming languages},
	publisher = {ACM},
	author = {Chen, Gang},
	month = jan,
	year = {2003},
	pages = {150--159},
}

@article{xue_theory_2013,
	title = {Theory and {Implementation} of {Coercive} {Subtyping}},
	language = {en},
	author = {Xue, Tao},
	year = {2013},
	file = {Xue - Theory and Implementation of Coercive Subtyping.pdf:/home/micha/Zotero/storage/D8NPAF3C/Xue - Theory and Implementation of Coercive Subtyping.pdf:application/pdf},
}

@article{luo_type-theoretical_2011,
	title = {Type-{Theoretical} {Semantics} with {Coercive} {Subtyping}},
	language = {en},
	author = {Luo, Zhaohui},
	year = {2011},
	file = {Luo - Type-Theoretical Semantics with Coercive Subtyping.pdf:/home/micha/Zotero/storage/3FYMAMJH/Luo - Type-Theoretical Semantics with Coercive Subtyping.pdf:application/pdf},
}

@article{cretin_power_2012,
	title = {On the {Power} of {Coercion} {Abstraction}},
	abstract = {Erasable coercions in System Fη, also known as retyping functions, are well-typed η-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in Fη can model subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain forms of delayed type instantiation. We generalize Fη by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the λ-calculus but keeping track of which parts of terms are coercions. We obtain a language where coercions do not contribute to the reduction but may block it and are thus not erasable. We recover erasable coercions by choosing a weak reduction strategy and restricting coercion abstraction to value-forms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes Fη, F{\textless}:, and MLF in a unified framework.},
	language = {en},
	author = {Cretin, Julien and Rémy, Didier},
	year = {2012},
	file = {Cretin and Rémy - On the Power of Coercion Abstraction.pdf:/home/micha/Zotero/storage/RWISHYPI/Cretin and Rémy - On the Power of Coercion Abstraction.pdf:application/pdf},
}

@inproceedings{eisenberg_closed_2014,
	address = {San Diego California USA},
	title = {Closed type families with overlapping equations},
	isbn = {978-1-4503-2544-8},
	url = {https://dl.acm.org/doi/10.1145/2535838.2535856},
	doi = {10.1145/2535838.2535856},
	abstract = {Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.},
	language = {en},
	urldate = {2024-09-10},
	booktitle = {Proceedings of the 41st {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {ACM},
	author = {Eisenberg, Richard A. and Vytiniotis, Dimitrios and Peyton Jones, Simon and Weirich, Stephanie},
	month = jan,
	year = {2014},
	pages = {671--683},
	file = {Eisenberg et al. - 2014 - Closed type families with overlapping equations.pdf:/home/micha/Zotero/storage/9LCHUC8M/Eisenberg et al. - 2014 - Closed type families with overlapping equations.pdf:application/pdf},
}

@article{mitchell_polymorphic_1988,
	title = {Polymorphic type inference and containment},
	volume = {76},
	copyright = {https://www.elsevier.com/tdm/userlicense/1.0/},
	issn = {08905401},
	url = {https://linkinghub.elsevier.com/retrieve/pii/0890540188900090},
	doi = {10.1016/0890-5401(88)90009-0},
	language = {en},
	number = {2-3},
	urldate = {2024-09-10},
	journal = {Information and Computation},
	author = {Mitchell, John C.},
	month = feb,
	year = {1988},
	pages = {211--249},
	file = {Mitchell - 1988 - Polymorphic type inference and containment.pdf:/home/micha/Zotero/storage/MKJNN5ZU/Mitchell - 1988 - Polymorphic type inference and containment.pdf:application/pdf},
}

@inproceedings{frisch_semantic_2002,
	address = {Copenhagen, Denmark},
	title = {Semantic subtyping},
	isbn = {978-0-7695-1483-3},
	url = {http://ieeexplore.ieee.org/document/1029823/},
	doi = {10.1109/LICS.2002.1029823},
	abstract = {Usually subtyping relations are defined either syntactically by a formal system or semantically by an interpretation of types in an untyped denotational model. In this work we show how to define a subtyping relation semantically, for a language whose operational semantics is driven by types; we consider a rich type algebra, with product, arrow, recursive, intersection, union and complement types. Our approach is to “bootstrap” the subtyping relation through a notion of set-theoretic model of the type algebra.},
	language = {en},
	urldate = {2024-09-10},
	booktitle = {Proceedings 17th {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {IEEE Comput. Soc},
	author = {Frisch, A. and Castagna, G. and Benzaken, V.},
	year = {2002},
	pages = {137--146},
	file = {Frisch et al. - 2002 - Semantic subtyping.pdf:/home/micha/Zotero/storage/94XXAY49/Frisch et al. - 2002 - Semantic subtyping.pdf:application/pdf},
}

@article{mitchell_coercion_1983,
	title = {Coercion and {Type} {Inference} ({Summary})},
	abstract = {A sinlple semantic model of automatic coercion is proposed. This modcl is used to explain four nlles for inferring polymorphic types and providing automatic coercions between types. With the addition ofa fifth rule. the rules become semantically c',mq{\textasciitilde}lete but the set of types associated with an expression may be undecidable. An cMcient type chcckio.g algorithm based on the Ih'st Ibur rules is presented. The algorithm is guaranteed to find a type whenever a type can be dedttccd ,sing the four inference rules. "1he type checking algorithm may be modi!icd so that calls to type conversion ftmctions are inserted at COmlfile time.},
	language = {en},
	author = {Mitchell, John C and Laboratories, Bell and Hill, Murray},
	year = {1983},
	file = {Mitchell et al. - Coercion and Type Inference (Summary).pdf:/home/micha/Zotero/storage/RIETWXT9/Mitchell et al. - Coercion and Type Inference (Summary).pdf:application/pdf},
}

@article{traytel_extending_2011,
	title = {Extending {Hindley}-{Milner} {Type} {Inference} with {Coercive} {Structural} {Subtyping} (long version)},
	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. Also, a sound but incomplete extension of the algorithm to type classes is given. The algorithm has been implemented in the proof assistant Isabelle.},
	language = {en},
	author = {Traytel, Dmitriy and Berghofer, Stefan and Nipkow, Tobias},
	year = {2011},
	file = {Traytel et al. - Extending Hindley-Milner Type Inference with Coerc.pdf:/home/micha/Zotero/storage/ZZCV89XY/Traytel et al. - Extending Hindley-Milner Type Inference with Coerc.pdf:application/pdf},
}

@article{mitchell_type_1991,
	title = {Type inference with simple subtypes},
	volume = {1},
	copyright = {https://www.cambridge.org/core/terms},
	issn = {0956-7968, 1469-7653},
	url = {https://www.cambridge.org/core/product/identifier/S0956796800000113/type/journal_article},
	doi = {10.1017/S0956796800000113},
	abstract = {Subtyping appears in a variety of programming languages, in the form of the "automatic coercion" of integers to reals, Pascal subranges, and subtypes arising from class hierarchies in languages with inheritance. A general framework based on untyped lambda calculus provides a simple semantic model of subtyping and is used to demonstrate that an extension of Curry’s type inference rules are semantically complete. An algorithm G for computing the most general typing associated with any given expression, and a restricted, optimized algorithm GA using only atomic subtyping hypotheses are developed. Both algorithms may be extended to insert type conversion functions at compile time or allow polymorphic function declarations as in ML.},
	language = {en},
	number = {3},
	urldate = {2024-09-10},
	journal = {Journal of Functional Programming},
	author = {Mitchell, John C.},
	month = jul,
	year = {1991},
	pages = {245--285},
	file = {Mitchell - 1991 - Type inference with simple subtypes.pdf:/home/micha/Zotero/storage/3TUX8NVG/Mitchell - 1991 - Type inference with simple subtypes.pdf:application/pdf},
}

@article{altenkirch_towards_2006,
	title = {Towards {Observational} {Type} {Theory}},
	abstract = {Observational Type Theory (OTT) combines beneficial aspects of Intensional and Extensional Type Theory (ITT/ETT). It separates definitional equality, decidable as in ITT, and a substitutive propositional equality, capturing extensional equality of functions, as in ETT. Moreover, canonicity holds: any closed term is definitionally reducible to a canonical value.},
	language = {en},
	author = {Altenkirch, Thorsten and McBride, Conor},
	year = {2006},
	file = {Altenkirch and McBride - Towards Observational Type Theory.pdf:/home/micha/Zotero/storage/LF2F3934/Altenkirch and McBride - Towards Observational Type Theory.pdf:application/pdf},
}

@article{eichholz_dependently-typed_2022,
	title = {Dependently-typed data plane programming},
	volume = {6},
	issn = {2475-1421},
	url = {https://dl.acm.org/doi/10.1145/3498701},
	doi = {10.1145/3498701},
	abstract = {Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of P4 code, especially as the language lacks basic safety guarantees. Type systems are a lightweight and compositional way to establish program properties, but there is a significant gap between the kinds of properties that can be proved using simple type systems (e.g., SafeP4) and those that can be obtained using full-blown verification tools (e.g., p4v). In this paper, we close this gap by developing Π4, a dependently-typed version of P4 based on decidable refinements. We motivate the design of Π4, prove the soundness of its type system, develop an SMT-based implementation, and present case studies that illustrate its applicability to a variety of data plane programs.},
	language = {en},
	number = {POPL},
	urldate = {2024-09-14},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Eichholz, Matthias and Campbell, Eric Hayden and Krebs, Matthias and Foster, Nate and Mezini, Mira},
	month = jan,
	year = {2022},
	pages = {1--28},
	file = {Eichholz et al. - 2022 - Dependently-typed data plane programming.pdf:/home/micha/Zotero/storage/Q65WWAU5/Eichholz et al. - 2022 - Dependently-typed data plane programming.pdf:application/pdf},
}

@article{crary_typed_2000,
	title = {Typed compilation of inclusive subtyping},
	abstract = {I present a type-preserving translation that eliminates subtyping and bounded quanti cation without introducing any run-time costs. This translation is based on Mitchell and Pierce's encoding of bounded quanti cation using intersection types. I show that, previous negative observations notwithstanding, the encoding is adequate given a su ciently rich target type theory. The necessary target type theory is made easily typecheckable by including a collection of explicit coercion combinators, which are already desired for eliminating subtyping. However, no form of coercion abstraction is necessary (even to support bounded quanti cation), leading to a simple target language.},
	language = {en},
	author = {Crary, Karl},
	year = {2000},
	file = {Crary - Typed compilation of inclusive subtyping.pdf:/home/micha/Zotero/storage/WSYG7E9K/Crary - Typed compilation of inclusive subtyping.pdf:application/pdf},
}