Daniel Ventura, PhD.
Assistant Professor (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: daniel at inf.ufg dot br

Research Interests

Curriculum Vitae: lattes.cnpq


Publications

See also: MathSciNet DBLP Scopus Google Scholar

Work in progress

  • F.L.C. de Moura, D.L. Ventura, R.S. Ramos and F.S. Paranhos. A constructive formalisation of the Modular Strong Normalisation Theorem.
    Submitted 2018. (pdf)

Journals

Conferences

  • 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



Teaching