A. Abel & B. Pientka (2016):
Well-founded recursion with copatterns and sized types.
JFP 26,
pp. e2,
doi:10.1017/S0956796816000022.
M. Avanzini & U. Dal Lago (2016):
Complexity Analysis by Polymorphic Sized Type Inference and Constraint Solving, Extended Version.
Technical Report.
Universities of Bologna and Innsbruck.
Available at http://cl-informatik.uibk.ac.at/users/zini/CAPSTICS.pdf..
Gilles Barthe, Benjamin Grégoire & Colin Riba (2008):
Type-Based Termination with Sized Products.
In: Proc. of 17th CSL,
LNCS 5213.
Springer,
pp. 493–507,
doi:10.1007/978-3-540-87531-4_35.
F. Blanqui (2005):
Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations.
In: Proc. of 14th CSL,
LNCS 3634.
Springer,
pp. 135–150,
doi:10.1007/11538363_11.
U. Dal Lago & M. Gaboardi (2011):
Linear Dependent Types and Relative Completeness.
LMCS 8(4),
doi:10.2168/LMCS-8(4:11)2012.
N. Danner, D. R. Licata & Ramyaa (2015):
Denotational Cost Semantics for Functional Languages with Inductive Types.
In: Proc. of 20th ICFP.
ACM,
pp. 140–151,
doi:10.1145/2858949.2784749.
J. Hoffmann, A. Das & S.-C. Weng (2017):
Towards Automatic Resource Bound Analysis for OCaml.
In: Proc. of 44th POPL.
ACM,
pp. 359–373,
doi:10.1145/3009837.3009842.
J. Hughes, L. Pareto & A. Sabry (1996):
Proving the Correctness of Reactive Systems Using Sized Types.
In: Proc. of 23rd POPL,
POPL '96.
ACM,
pp. 410–423,
doi:10.1145/237721.240882.
A. Mycroft (1984):
Polymorphic Type Schemes and Recursive Definitions,
pp. 217–228.
Springer.
P. Vasconcelos (2008):
Space Cost Analysis Using Sized Types.
School of Computer Science, University of St Andrews.
eptcs@eptcs.org