Daniel Ventura, PhD.
Associate Professor (Senior Lecturer)
Formal Structures, Foundations and Applications
Institute of Informatics
Goiás Federal University

Address:
Instituto de Informática, Universidade Federal de Goiás
Alameda Palmeiras, Quadra D, Campus Samambaia
74690-900 Goiania GO, Brasil
Tel. +55-62-3521-1181
Fax +55-62-3521-1182
e-mail: ventura at ufg dot br

Research Interests

Curriculum Vitae: lattes.cnpq

Publications

See also: MathSciNet DBLP Scopus Google Scholar

Work in progress

Journals

Conferences

  • S. Alves and D. Ventura. Quantitative Weak Linearisation.
    Proc. of the 19th Int. Colloquium on Theoretical Aspects of Computing (ICTAC), Tbilisi, Georgia, September 27-29, 2022.
    LNCS 13572:78-95, 2022.
    (pdf) © Springer Nature Switzerland AG.

  • D. Nantes-Sobrinho, C. Olarte and D. Ventura. A subexponential view of domains in session types.
    Proc. of the 16th Int. Workshop on Logical and Semantical Frameworks, with Applications (LSFA), Buenos Aires, Argentina, July 2021.
    EPTCS 357, 2022, pp. 93-111.
    (pdf)

  • D. Kesner, L. Peyrot and D. Ventura. The Spirit of Node Replication.
    Proc. of the 23rd Int. Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
    LNCS 12650, pages 344--364, Luxembourg, Luxembourg, March-April 2021.
    (pdf) © LNCS.

  • S. Alves, D. Nantes-Sobrinho, J.A. Pérez and D. Ventura. An Investigation of Linear Substitution λ-Calculus as Session-Typed Processes (short paper).
    The 15th Int. Workshop on Logical and Semantical Frameworks, with Applications (LSFA), Salvador, Brazil, August 2020.
    (pdf)

  • S. Alves, D. Kesner and D. Ventura. A Quantitative Understanding of Pattern Matching.
    Post-Proc of the 25th International Conference on Types for Proofs and Programs (TYPES).
    LIPIcs, Vol 175, pages 3:1--3:36, Oslo, Norway, June 2019.
    (pdf) © LIPIcs.

  • A. Bucciarelli and D. Kesner and D. Ventura. Strong Normalization through Intersection Types and Memory.
    Proc. of the 10th Int. Workshop on Logical and Semantical Frameworks, with Applications (LSFA), Natal, Brazil, August-September 2015.
    ENTCS 323:75-91, 2016.
    (pdf) © Elsevier Science B. V.

  • F. Kamareddine, J. Wells and D. Ventura. Automath Type Inclusion in Barendregt’s Cube.
    Proc. of the 10th International Computer Science Symposium in Russia (CSR), Listvyanka, Russia, July 2015.
    LNCS 9139:262-282, 2015.

  • D. Kesner and D. Ventura. A resource aware computational interpretation for Herberlin's syntax.
    Proc. of the 12th Int. Colloquium on Theoretical Aspects of Computing (ICTAC), Cali, Colombia, September 2015.
    LNCS 9399:1-16, 2015.
    (pdf) © Springer-Verlag.

  • D. Kesner and D. Ventura. Quantitative Types for the Linear Substitution Calculus.
    Proc. of the 8th Int. Conference on Theoretical Computer Science (TCS), Rome, Italy, September 2014.
    LNCS 8705:296-310, 2014.
    (pdf) © Springer-Verlag.

  • W.L.R. de C. Segundo, F.L.C. de Moura and D.L. Ventura. Formalizing a Named Explicit Substitutions Calculus in Coq.
    Proc. of the Work in Progress Section of Conferences on Intelligent Computer Mathematics (CICM-WS-WiP), Coimbra, Portugal, July 2014.
    CEUR-WS 1186 (pdf, Coq files)

  • D. Ventura, D. Kesner and A. Bucciarelli. A combinatorial argument for termination properties.
    Proc. of the 17th Brazilian Logic Conference (EBL), Petrópolis, Brazil, 2014.
    Book of Abstracts pp. 105.

  • D.L. Ventura, M. Ayala-Rincón and F. Kamareddine. Intersection types and explicit substitution.
    15th Latin American Symposium on Mathematical Logic (SLALM), Bogotá, Colombia, June 2012.
    Book of Abstracts pp. 53.

  • D.L. Ventura, M. Ayala-Rincón and F. Kamareddine. Towards a characterisation of termination for explicit substitution calculi with de Bruijn indices.
    Proc. of the 16th Brazilian Logic Conference (EBL), Petrópolis, Brazil, May 2011.
    Book of Abstracts pp. 66.

  • D. Ventura, M. Ayala-Rincón and F. Kamareddine. Intersection Type Systems and Explicit Substitutions Calculi.
    Proc. of the 17th Workshop on Logic, Language, Information and Computation (WoLLIC), Brasília, Brazil, July 2010.
    LNCS (FoLLI-LNAI subseries) 6188:232-246, 2010.

  • D. Ventura, M. Ayala-Rincón and F. Kamareddine. Principal typings in a restricted intersection type system for beta normal forms with de Bruijn indices.
    Proc. of the 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS), Brasília, Brazil, June 2009.
    EPTCS 15:69-82, 2010.

  • D. Ventura, M. Ayala-Rincón and F. Kamareddine. Principal Typings for Explicit Substitutions calculi.
    Proc. of the 4th Conference on Computability in Europe (CiE), Athens, Greece, June 2008.
    LNCS 5028:567-578, 2008.
    (pdf) ©Springer-Verlag.

  • D. Ventura, M. Ayala-Rincón and F. Kamareddine. Intersection Type Systems with de Bruijn Indices.
    Proc. of the 30th Anniversary of the Centre for Logic, Epistemology and the History of Science, UNICAMP (CLE), 15th Brazilian Logic Conference (EBL) and 14th Latin-American Symposium on Mathematical Logic (SLALM), Paraty, Brazil, May 2008.
    (extended version pdf)

    Revised version published as book chapter in Studies in Logic Series v. 21 (The Many Sides of Logic), pp. 557-576, 2009.

  • D. Ventura, M. Ayala-Rincón and F. Kamareddine. Principal Typing for Explicit Substitutions Calculi.
    Proc. of the 4th Int. Workshop on Higher-Order Rewriting (HOR), Paris, France, June 2007.
    (extended version pdf).

  • D. Ventura, M. Ayala-Rincón and F. Kamareddine. Explicit Substitutions Calculi with Explicit Eta rules which Preserve Subject Reduction.
    Proc. of the 1st Workshop on Logical and Semantic Frameworks, with Applications (LSFA). Natal, Brazil, September 2006.

Others

Professional Activities

Teaching