Non-idempotent intersection types for the lambda-calculus A Bucciarelli, D Kesner, D Ventura Logic Journal of the IGPL 25 (4), 431-464, 2017 | 44 | 2017 |
Quantitative types for the linear substitution calculus D Kesner, D Ventura IFIP International Conference on Theoretical Computer Science, 296-310, 2014 | 32 | 2014 |
A resource aware computational interpretation for herbelin’s syntax D Kesner, D Ventura International Colloquium on Theoretical Aspects of Computing, 388-403, 2015 | 13 | 2015 |
Strong normalization through intersection types and memory A Bucciarelli, D Kesner, D Ventura Electronic Notes in Theoretical Computer Science 323, 75-91, 2016 | 9 | 2016 |
Intersection type system with de Bruijn indices D Ventura, M Ayala-Rincón, F Kamareddine The many sides of logic. Studies in logic 21, 557-576, 2008 | 7 | 2008 |
Quantitative types for intuitionistic calculi D Kesner, D Ventura | 6 | 2014 |
Principal typings in a restricted intersection type system for beta normal forms with de Bruijn indices D Ventura, M Ayala-Rincón, F Kamareddine arXiv preprint arXiv:1001.4438, 2010 | 4 | 2010 |
Principal typings for explicit substitutions calculi DL Ventura, M Ayala-Rincón, F Kamareddine Conference on Computability in Europe, 567-578, 2008 | 4 | 2008 |
Explicit substitution calculi with de Bruijn indices and intersection type systems DL Ventura, F Kamareddine, M Ayala-Rincón Logic Journal of the IGPL 23 (2), 295-340, 2015 | 3 | 2015 |
Intersection type systems and explicit substitutions calculi DL Ventura, M Ayala-Rincón, F Kamareddine International Workshop on Logic, Language, Information, and Computation, 232-246, 2010 | 3 | 2010 |
A resource aware semantics for a focused intuitionistic calculus D Kesner, D Ventura Mathematical Structures in Computer Science 29 (1), 93-126, 2019 | 2 | 2019 |
A combinatorial argument for termination properties DL Ventura, A Bucciarelli, D Kesner The Brazilian Logic Conference (EBL), 2013 | 2 | 2013 |
Cálculos de substituições explícitas à la de Bruijn com sistemas de tipos com interseção DL Ventura | 2 | 2010 |
Nominal essential intersection types M Ayala-Rincón, M Fernández, AC Rocha-Oliveira, DL Ventura Theoretical Computer Science 737, 62-80, 2018 | 1 | 2018 |
An Investigation of Linear Substitution λ-Calculus as Session-Typed Processes S Alves, D Nantes-Sobrinho, JA Pérez, D Ventura Pre-Proceedings, 115, 2020 | | 2020 |
A Quantitative Understanding of Pattern Matching S Alves, D Kesner, D Ventura arXiv preprint arXiv:1912.01914, 2019 | | 2019 |
Automath type inclusion in Barendregt’s Cube F Kamareddine, JB Wells, D Ventura International Computer Science Symposium in Russia, 262-282, 2015 | | 2015 |
Explicit substitutions calculi with one step Eta-reduction decided explicitly D Ventura, M Ayala-Rincón, F Kamareddine Logic Journal of the IGPL 17 (6), 697-718, 2009 | | 2009 |
A Quantitative Understanding of Pattern S Alves, D Kesner, D Ventura | | |
Formalizing a Named Explicit Substitutions Calculus in Coq WLRC Segundo, FLC de Moura, DL Ventura | | |