Algorithmic Introduction of Quantified Cuts (submitted). Stefan Hetzl, Alexander Leitsch, Giselle Reis and Daniel Weller, Theoretical Computer Science 2013
An Extended Framework for Specifying and Reasoning about Proof Systems (submitted). Vivek Nigam, Elaine Pimentel and Giselle Reis, Journal of Logic and Computation (Special Issue in honour of Roy Dyckhoff) 2013
Towards CERes in intuitionistic logic. Alexander Leitsch, Giselle Reis
and Bruno W. Paleo, CSL 2012 Proceedings.
[pdf]
Specifying proof systems in linear logic with subexponentials. Vivek
Nigam, Elaine Pimentel and Giselle Reis, LSFA 2010, published in ENTCS.
[pdf]
Using Linear Logic with Subexponentials to Implement Logic Interpreters. Giselle Reis and Elaine Pimentel, SBMF 2010.
[pdf]
Projects:
QUATI: Online system for checking permutation of
sequent calculus rules (under development).
TATU: Online system for reasoning about sequent
calculus specifications in linear logic with subexponentials.
GAPT: Generic Architecture for
Proof Transformations
SELLF system:
Implementation of Linear Logic with Subexponentials
SELLF and other systems in l-Prolog (tar.gz): Simple implementation of
Linear Logic with Subexponentials and the specification of some systems in SELLF. Implemented
during my master's degree.
Checking Proof Transformations with ASP (presentation of paper) ICLP 2013
Istanbul, Turkey, 24-29 August, 2013
A framework for specifying and reasoning in sequent calculus systems UNILOG 2013 - Workshop on Compositional Meaning in Logic (GeTFun 1.0)
Rio de Janeiro, Brazil, 3-4 April 2013
Using Linear Logic with Subexponentials to Implement Logic Interpreters (presentation of paper - best paper) SBMF (13th Brazilian Symposium on Formal Methods - Workshop on Thesis and Dissertations)
Natal, Brazil, 8-12 November 2010
