Document Open Access Logo

Types as Resources for Classical Natural Deduction

Authors Delia Kesner, Pierre Vial

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.24.pdf
  • Filesize: 0.53 MB
  • 17 pages

Document Identifiers

Author Details

Delia Kesner
Pierre Vial

Cite AsGet BibTex

Delia Kesner and Pierre Vial. Types as Resources for Classical Natural Deduction. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.24

Abstract

We define two resource aware typing systems for the lambda-mu-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments - based on decreasing measures of type derivations - to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the length of head-reduction sequences and maximal reduction sequences.
Keywords
  • lambda-mu-calculus
  • classical logic
  • intersection types
  • normalization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Peter Sewell, editor, Proceedings of the 41st Annual ACM Symposium on Principles of Programming Languages (POPL), pages 659-670. ACM Press, 2014. Google Scholar
  2. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Anuj Dawar and Helmut Veith, editors, Proceedings of 24th EACSL Conference on Computer Science Logic, volume 6247 of Lecture Notes in Computer Science, pages 381-395. Springer-Verlag, August 2010. Google Scholar
  3. Shahin Amini and Thomas Erhard. On Classical PCF, Linear Logic and the MIX Rule. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), volume 41 of Leibniz International Proceedings in Informatics (LIPIcs), pages 582-596. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  4. Zena M. Ariola, Hugo Herbelin, and Alexis Saurin. Classical call-by-need and duality. In Luke Ong [31], pages 27-44. Google Scholar
  5. Alexis Bernadet and Stéphane Lengrand. Complexity of strongly normalising λ-terms via non-idempotent intersection types. In Martin Hofmann, editor, Foundations of Software Science and Computation Structures (FOSSACS), volume 6604 of Lecture Notes in Computer Science, pages 88-107. Springer-Verlag, 2011. Google Scholar
  6. Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. Google Scholar
  7. Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In Díaz et al. [16], pages 341-354. Google Scholar
  8. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 2017. Google Scholar
  9. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for lambda-terms. Archive for Mathematical Logic, 19:139-156, 1978. Google Scholar
  10. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 4:685-693, 1980. Google Scholar
  11. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montreal, Canada, September 18-21, 2000, pages 233-243. ACM, 2000. Google Scholar
  12. René David and Karim Nour. A short proof of the strong normalization of classical natural deduction with disjunction. J. Symb. Log., 68(4):1277-1288, 2003. Google Scholar
  13. Erika De Benedetti and Simona Ronchi Della Rocca. Bounding normalization time through intersection types. In Graham-Lengrand and Paolini [21], pages 48-57. Google Scholar
  14. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. These de doctorat, Université Aix-Marseille II, 2007. Google Scholar
  15. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009. Google Scholar
  16. Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors. Proceedings of the 8th International Conference on Theoretical Computer Science (TCS), volume 8705 of Lecture Notes in Computer Science. Springer-Verlag, 2014. Google Scholar
  17. Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne. Characterizing strong normalization in the curien-herbelin symmetric lambda calculus: Extending the coppo-dezani heritage. Theoretical Computer Science, 398(1-3):114-128, 2008. Google Scholar
  18. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, Proceedings of 26th EACSL Conference on Computer Science Logic, volume 16 of LIPIcs, pages 259-273. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. Google Scholar
  19. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, International Conference TACS'94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 555-574. Springer, 1994. Google Scholar
  20. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1990. Google Scholar
  21. Stéphane Graham-Lengrand and Luca Paolini, editors. Proceedings of the Sixth Workshop on Intersection Types and Related Systems (ITRS), Dubrovnik, Croatia, 2012, volume 121 of Electronic Proceedings in Theoretical Computer Science, 2013. Google Scholar
  22. Timothy Griffin. A formulae-as-types notion of control. In 17th Annual ACM Symposium on Principles of Programming Languages (POPL), pages 47-58. ACM Press, 1990. Google Scholar
  23. Delia Kesner. Reasoning about call-by-need by means of types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 424-441. Springer-Verlag, 2016. Google Scholar
  24. Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In Díaz et al. [16], pages 296-310. Google Scholar
  25. Delia Kesner and Daniel Ventura. A resource aware computational interpretation for herbelin’s syntax. In Martin Leucker, Camilo Rueda, and Frank D. Valencia, editors, Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, volume 9399 of Lecture Notes in Computer Science, pages 388-403. Springer-Verlag, 2015. Google Scholar
  26. Delia Kesner and Pierre Vial. Types as resources for classical natural deduction, 2017. Available at URL: http://www.irif.fr/~kesner/papers/lambda-mu.pdf.
  27. Assaf Kfoury. A linearization of the lambda-calculus and consequences. Technical report, Boston Universsity, 1996. Google Scholar
  28. Kentaro Kikuchi and Takafumi Sakurai. A translation of intersection and union types for the λμ-calculus. In Jacques Garrigue, editor, Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, volume 8858 of Lecture Notes in Computer Science, pages 120-139. Springer-Verlag, 2014. Google Scholar
  29. Jean-Louis Krivine. Lambda-calculus, types and models. Ellis Horwood, 1993. Google Scholar
  30. Olivier Laurent. On the denotational semantics of the untyped lambda-mu calculus, 2004. Unpublished note. Google Scholar
  31. C.-H. Luke Ong, editor. Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science. Springer-Verlag, 2011. Google Scholar
  32. Michel Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, International Conference on Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer-Verlag, July 1992. Google Scholar
  33. Pierre-Marie Pédrot and Alexis Saurin. Classical by-need. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 616-643. Springer-Verlag, 2016. Google Scholar
  34. Peter Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science, 11(2):207-260, 2001. Google Scholar
  35. Pawel Urzyczyn. The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195-1215, 1999. Google Scholar
  36. Steffen van Bakel. Sound and complete typing for lambda-mu. In Elaine Pimentel, Betti Venneri, and Joe B. Wells, editors, Proceedings Fifth Workshop on Intersection Types and Related Systems, ITRS 2010, Edinburgh, U.K., 9th July 2010, volume 45 of EPTCS, pages 31-44, 2010. Google Scholar
  37. Steffen van Bakel, Franco Barbanera, and Ugo de'Liguoro. A filter model for the λμ-calculus - (extended abstract). In Luke Ong [31], pages 213-228. Google Scholar
  38. Steffen van Bakel, Franco Barbanera, and Ugo de'Liguoro. Characterisation of strongly normalising lambda-mu-terms. In Graham-Lengrand and Paolini [21], pages 1-17. Google Scholar
  39. Lionel Vaux. Convolution lambda-bar-mu-calculus. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of Lecture Notes in Computer Science, pages 381-395. Springer-Verlag, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact