
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, AugustSeptember 2015.
ENTCS 323:7591, 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:262282, 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:116, 2015.
(pdf) © SpringerVerlag.

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:296310, 2014.
(pdf) © SpringerVerlag.

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 (CICMWSWiP), Coimbra, Portugal, July 2014.
CEURWS 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. AyalaRincó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. AyalaRincó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. AyalaRincó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 (FoLLILNAI subseries) 6188:232246, 2010.

D. Ventura,
M. AyalaRincó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:6982, 2010.

D. Ventura,
M. AyalaRincó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:567578, 2008.
(pdf) ©SpringerVerlag.

D. Ventura,
M. AyalaRincó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 LatinAmerican
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. 557576, 2009.

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

D. Ventura,
M. AyalaRincó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.
