@article(AP:JFP:16,
 author       = {A. Abel and B. Pientka},
 year         = {2016},
 title        = {{Well-founded recursion with copatterns and sized types}},
 journal      = {JFP},
 volume       = {26},
 pages        = {e2},
 doi          = {10.1017/S0956796816000022},
)
@techreport(EV,
 author       = {M. Avanzini and {Dal Lago}, U.},
 year         = {2016},
 title        = {{Complexity Analysis by Polymorphic Sized Type Inference and Constraint Solving, Extended Version}},
 type         = {Technical Report},
 institution  = {Universities of Bologna and Innsbruck},
 note         = {Available at \url{http://cl-informatik.uibk.ac.at/users/zini/CAPSTICS.pdf}.},
)
@inproceedings(GBR:CSL:08,
 author       = {Gilles Barthe and Benjamin Gr{\'{e}}goire and Colin Riba},
 year         = {2008},
 title        = {{Type-Based Termination with Sized Products}},
 booktitle    = {Proc.\ of\ \ensuremath{\text{17}^{\text{th}}} CSL},
 series       = {LNCS},
 volume       = {5213},
 publisher    = {Springer},
 pages        = {493--507},
 doi          = {10.1007/978-3-540-87531-4_35},
)
@inproceedings(Blanqui:CSL:05,
 author       = {F. Blanqui},
 year         = {2005},
 title        = {{Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations}},
 booktitle    = {Proc.\ of\ \ensuremath{\text{14}^{\text{th}}} CSL},
 series       = {LNCS},
 volume       = {3634},
 publisher    = {Springer},
 pages        = {135--150},
 doi          = {10.1007/11538363_11},
)
@article(LG:LMCS:11,
 author       = {{Dal Lago}, U. and M. Gaboardi},
 year         = {2011},
 title        = {{Linear Dependent Types and Relative Completeness}},
 journal      = {LMCS},
 volume       = {8},
 number       = {4},
 doi          = {10.2168/LMCS-8(4:11)2012},
)
@inproceedings(DLR:ICFP:15,
 author       = {N. Danner and D. R. Licata and Ramyaa},
 year         = {2015},
 title        = {{Denotational Cost Semantics for Functional Languages with Inductive Types}},
 booktitle    = {Proc.\ of \ensuremath{\text{20}^{\text{th}}} ICFP},
 publisher    = {ACM},
 pages        = {140--151},
 doi          = {10.1145/2858949.2784749},
)
@inproceedings(HDW:POPL:17,
 author       = {J. Hoffmann and A. Das and S.-C. Weng},
 year         = {2017},
 title        = {{Towards Automatic Resource Bound Analysis for OCaml}},
 booktitle    = {Proc.\ of\ \ensuremath{\text{44}^{\text{th}}} POPL},
 publisher    = {ACM},
 pages        = {359--373},
 doi          = {10.1145/3009837.3009842},
)
@inproceedings(HPS:POPL:96,
 author       = {J. Hughes and L. Pareto and A. Sabry},
 year         = {1996},
 title        = {{Proving the Correctness of Reactive Systems Using Sized Types}},
 booktitle    = {Proc.\ of\ \ensuremath{\text{23}^{\text{rd}}} POPL},
 series       = {POPL '96},
 publisher    = {ACM},
 pages        = {410--423},
 doi          = {10.1145/237721.240882},
)
@inbook(Mycroft:ISP:84,
 author       = {A. Mycroft},
 year         = {1984},
 title        = {{Polymorphic Type Schemes and Recursive Definitions}},
 pages        = {217--228},
 publisher    = {Springer},
)
@phdthesis(Vasconcelos:Diss:08,
 author       = {P. Vasconcelos},
 year         = {2008},
 title        = {{Space Cost Analysis Using Sized Types}},
 school       = {School of Computer Science, University of St Andrews},
)