Linear Sized Types in the Calculus of Constructions

1. Abel, A.: A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München (2006)

   Google Scholar 

2. Abel, A.: Semi-continuous sized types and termination. Logical Methods in Computer Science 4(2) (2008)

   Google Scholar 

3. Abel, A.: MiniAgda: Integrating sized and dependent types. In: Bove, A., Komendantskaya, E., Niqui, M. (eds.) PAR (2010)

   Google Scholar 

4. Abel, A., Pientka, B.: Wellfounded recursion with copatterns: a unified approach to termination and productivity. In: Morrisett, G., Uustalu, T. (eds.) ICFP, pp. 185–196. ACM (2013)

   Google Scholar 

5. Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 27–38. ACM (2013)

   Google Scholar 

6. Altenkirch, T.: Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh (November 1993)

   Google Scholar 

7. Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, pp. 117–309. Oxford Science Publications (1992)

   Google Scholar 

8. Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14(1), 97–141 (2004)

   Article  MATH  MathSciNet  Google Scholar 

9. Barthe, G., Grégoire, B., Pastawski, F.: Practical inference for type-based termination in a polymorphic setting. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 71–85. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

10. Barthe, G., Grégoire, B., Pastawski, F.: CIC\(\widehat{~}\): Type-based termination of recursive definitions in the Calculus of Inductive Constructions. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 257–271. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

11. Barthe, G., Grégoire, B., Riba, C.: Type-based termination with sized products. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 493–507. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

12. Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 24–39. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

13. Blanqui, F., Riba, C.: Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 105–119. Springer, Heidelberg (2006)

    Google Scholar 

14. Endrullis, J., Grabmayer, C., Hendriks, D.: Data-oblivious stream productivity. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 79–96. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

15. Endrullis, J., Grabmayer, C., Hendriks, D., Isihara, A., Klop, J.W.: Productivity of stream definitions. Theor. Comput. Sci. 411(4-5), 765–782 (2010)

    Article  MATH  MathSciNet  Google Scholar 

16. Giménez, E.: A Calculus of Infinite Constructions and its application to the verification of communicating systems. PhD thesis, Ecole Normale Supérieure de Lyon (1996)

    Google Scholar 

17. Grégoire, B., Sacchini, J.L.: On strong normalization of the calculus of constructions with type-based termination. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 333–347. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

18. Hermann, M., Voronkov, A. (eds.): LPAR 2006. LNCS (LNAI), vol. 4246. Springer, Heidelberg (2006)

    MATH  Google Scholar 

19. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL, pp. 410–423 (1996)

    Google Scholar 

20. McBride, C.: Let’s see how things unfold: Reconciling the infinite with the intensional (extended abstract). In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 113–126. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

21. Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)

    Google Scholar 

22. Pareto, L.: Types for Crash Prevention. PhD thesis, Chalmers University of Technology (2000)

    Google Scholar 

23. Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Martin, J.L. (ed.) SC, pp. 4–13. IEEE Computer Society/ACM (1991)

    Google Scholar 

24. Sacchini, J.L.: On Type-Based Termination and Dependent Pattern Matching in the Calculus of Inductive Constructions. PhD thesis, École Nationale Supérieure des Mines de Paris (2011)

    Google Scholar 

25. Sacchini, J.L.: Type-based productivity of stream definitions in the calculus of constructions. In: LICS, pp. 233–242. IEEE Computer Society (2013)

    Google Scholar 

26. Sacchini, J.L.: Linear sized types in the calculus of constructions. Technical Report CMU-CS-14-104, Carnegie Mellon University (2014)

    Google Scholar 

27. Setzer, A.: Coalgebras as types determined by their elimination rules. In: Dybjer, P., Lindström, S., Palmgren, E., Sundholm, G. (eds.) Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science, vol. 27, pp. 351–369. Springer (2012)

    Google Scholar 

28. The Coq Development Team. The Coq Reference Manual, version 8.4 (2012)

    Google Scholar 

29. Pedro, B.: Vasconcelos. Space cost analysis using sized types. PhD thesis, University of St. Andrews (2008)

    Google Scholar 

Download references