publications.bib

@article{OlarteLSFA17,
  author = {Bruno Xavier and Carlos Olarte and Giselle Reis and Vivek Nigam},
  title = {{Mechanizing Focused Linear Logic in Coq}},
  journal = {Electronic Notes in Theoretical Computer Science},
  note = {The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017)},
  volume = {338},
  pages = {219 -- 236},
  year = {2018},
  issn = {1571-0661},
  doi = {10.1016/j.entcs.2018.10.014},
  url = {http://www.gisellereis.com/papers/ll-coq.pdf}
}

@article{ChaudhuriTCS17,
  author = {Kaustuv Chaudhuri and Leonardo Lima and Giselle Reis},
  title = {{Formalized Meta-Theory of Sequent Calculi for Substructural Logics}},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {332},
  pages = {57 -- 73},
  year = {2017},
  note = {LSFA 2016 - 11th Workshop on Logical and Semantic Frameworks with Applications (LSFA)},
  issn = {1571-0661},
  doi = {10.1016/j.entcs.2017.04.005},
  url = {http://www.gisellereis.com/papers/ll-abella-long.pdf}
}

@article{ReisMSCS17,
  author = {Giselle Reis and Bruno Woltzenlogel Paleo},
  title = {{Complexity of Translations from Resolution to Sequent Calculus}},
  journal = {Mathematical Structures in Computer Science},
  publisher = {Cambridge University Press},
  pages = {1–31},
  year = {2018},
  doi = {10.1017/S0960129518000476},
  url = {http://www.gisellereis.com/papers/res-seq-translations.pdf}
}

@article{EbnerJAR18,
  author = {Gabriel Ebner and Stefan Hetzl and Alexander Leitsch and Giselle Reis and Daniel Weller},
  title = {{On the Generation of Quantified Lemmas}},
  journal = {Journal of Automated Reasoning},
  year = {2018},
  issn = {1573-0670},
  doi = {10.1007/s10817-018-9462-8},
  url = {http://www.gisellereis.com/papers/cut-intro-long.pdf}
}

@article{CernaAPAL17,
  author = {David Cerna and Alexander Leitsch and Giselle Reis and Simon Wolfsteiner},
  title = {{Ceres in intuitionistic logic}},
  journal = {Annals of Pure and Applied Logic},
  volume = {168},
  number = {10},
  pages = {1783 -- 1836},
  year = {2017},
  issn = {0168-0072},
  doi = {10.1016/j.apal.2017.04.001},
  url = {http://www.gisellereis.com/papers/ceres-lj.pdf}
}

@article{ReisEpsilon17,
  author = {Giselle Reis and Bruno Woltzenlogel Paleo},
  title = {{Epsilon Terms in Intuitionistic Sequent Calculus}},
  journal = {IfCoLog Journal of Logics and their Applications, Special Issue: Hilberts epsilon and tau in Logic, Informatics and Linguistics},
  volume = {4},
  number = {2},
  pages = {401 -- 423},
  year = {2017},
  isbn = {978-1-84890-234-3},
  doi = {http://www.collegepublications.co.uk/downloads/ifcolog00011.pdf},
  url = {http://www.gisellereis.com/papers/lj-epsilon.pdf}
}

@article{HetzlTCS14,
  author = {Stefan Hetzl and Alexander Leitsch and Giselle Reis and Daniel Weller},
  title = {{Algorithmic introduction of quantified cuts}},
  journal = {Theoretical Computer Science},
  volume = {549},
  pages = {1 -- 16},
  year = {2014},
  note = {A more complete version can be found at \url{https://arxiv.org/abs/1401.4330}},
  issn = {0304-3975},
  doi = {10.1016/j.tcs.2014.05.018},
  url = {http://www.gisellereis.com/papers/cut-intro-tcs.pdf}
}

@article{NigamJLC16,
  author = {Vivek Nigam and Elaine Pimentel and Giselle Reis},
  title = {{An extended framework for specifying and reasoning about proof systems}},
  journal = {Journal of Logic and Computation},
  volume = {26},
  number = {2},
  pages = {539-576},
  year = {2016},
  doi = {10.1093/logcom/exu029},
  url = {http://www.gisellereis.com/papers/modal-sellf.pdf}
}

@misc{KarkourTYPES23,
  author = {Ammar Karkour and Giselle Reis},
  title = {A Formalization of Python's Execution Machinery},
  howpublished = {29$^{th}$ International Conference on Types for Proofs and Programs (TYPES)},
  year = {2023},
  url = {http://www.gisellereis.com/papers/pystar-types.pdf}
}

@misc{ShaheerTYPES23,
  author = {Mohammad Shaheer and Giselle Reis and Bruno Woltzenlogel Paleo and Joachim Zahnentferner},
  title = {Formalization of Blockchain Oracles in Coq},
  howpublished = {29$^{th}$ International Conference on Types for Proofs and Programs (TYPES)},
  year = {2023},
  url = {http://www.gisellereis.com/papers/oracles-types.pdf}
}

@inproceedings{lfmtpInv,
  author = {Reis, Giselle},
  year = {2021},
  title = {{Facilitating Meta-Theory Reasoning (Invited Paper)}},
  editor = {Pimentel, Elaine and Tassi, Enrico},
  booktitle = {Proceedings Sixteenth Workshop on
               Logical Frameworks and Meta-Languages: Theory and Practice},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {337},
  publisher = {Open Publishing Association},
  pages = {1-12},
  doi = {10.4204/EPTCS.337.1},
  url = {https://gisellereis.com/papers/meta-reasoning.pdf}
}

@inproceedings{smlToCoq,
  author = {El-Beheiry, Laila and Reis, Giselle and Karkour, Ammar},
  year = {2021},
  title = {{SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts}},
  editor = {Pimentel, Elaine and Tassi, Enrico},
  booktitle = {Proceedings Sixteenth Workshop on
               Logical Frameworks and Meta-Languages: Theory and Practice},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {337},
  publisher = {Open Publishing Association},
  pages = {71-87},
  doi = {10.4204/EPTCS.337.6},
  url = {https://gisellereis.com/papers/sml-to-coq.pdf}
}

@inproceedings{Cyberlogic,
  author = {Nigam, Vivek and Reis, Giselle and Rahmouni, Samar and Ruess, Harald},
  editor = {Platzer, Andr{\'e} and Sutcliffe, Geoff},
  title = {{Proof Search and Certificates for Evidential Transactions}},
  booktitle = {Automated Deduction -- CADE 28},
  year = {2021},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {234--251},
  isbn = {978-3-030-79876-5},
  doi = {10.1007/978-3-030-79876-5_14},
  url = {https://gisellereis.com/papers/cyberlogic.pdf}
}

@inproceedings{Sequoia,
  author = {Reis, Giselle and Naeem, Zan and Hashim, Mohammed},
  editor = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
  title = {{Sequoia: A Playground for Logicians}},
  booktitle = {10$^{th}$ International Joint Conference on Automated Reasoning, (IJCAR)},
  year = {2020},
  publisher = {Springer International Publishing},
  pages = {480--488},
  doi = {10.1007/978-3-030-51054-1_32},
  url = {http://www.gisellereis.com/papers/sequoia.pdf}
}

@misc{NaeemUNIF19,
  author = {Zan Naeem and Giselle Reis},
  title = {Unification of Multisets with Multiple Labelled Multiset Variables},
  howpublished = {33$^{rd}$ International Workshop on Unification (UNIF)},
  year = {2019},
  url = {http://www.gisellereis.com/papers/mset-unif.pdf}
}

@inproceedings{CervesatoLinearity18,
  author = {Iliano Cervesato and Sharjeel Khan and Giselle Reis and Dragisa Zunic},
  title = {{Formalization of Automated Trading Systems in a Concurrent Linear Framework}},
  booktitle = {Proceedings Joint International Workshop on Linearity {\&} Trends
               in Linear Logic and Applications, Linearity-TLLA@FLoC},
  pages = {1--14},
  year = {2018},
  doi = {10.4204/EPTCS.292.1},
  url = {http://www.gisellereis.com/papers/fin-clf.pdf}
}

@inproceedings{OlarteLinearity18,
  author = {Carlos Olarte and Valeria de Paiva and Elaine Pimentel and Giselle Reis},
  title = {{The ILLTP Library for Intuitionistic Linear Logic}},
  booktitle = {Proceedings Joint International Workshop on Linearity {\&} Trends
               in Linear Logic and Applications, Linearity-TLLA@FLoC},
  pages = {118--132},
  year = {2018},
  doi = {10.4204/EPTCS.292.7},
  url = {http://www.gisellereis.com/papers/lltp.pdf}
}

@inproceedings{EbnerIJCAR16,
  author = {Gabriel Ebner and Stefan Hetzl and Giselle Reis and Martin Riener and Simon Wolfsteiner and Sebastian Zivota},
  title = {{System Description: GAPT 2.0}},
  booktitle = {8$^{th}$ International Joint Conference on Automated Reasoning, (IJCAR)},
  pages = {293--301},
  year = {2016},
  doi = {10.1007/978-3-319-40229-1_20},
  url = {http://www.gisellereis.com/papers/gapt.pdf}
}

@inproceedings{ChaudhuriLSFA17,
  author = {Kaustuv Chaudhuri and Leonardo Lima and Giselle Reis},
  title = {{Formalized Meta-Theory of Sequent Calculi for Substructural Logics}},
  booktitle = {11$^{th}$ Workshop on Logical and Semantic Frameworks with Applications (LSFA)},
  volume = {332},
  pages = {57 -- 73},
  year = {2016},
  issn = {1571-0661},
  doi = {10.1016/j.entcs.2017.04.005},
  url = {http://www.gisellereis.com/papers/ll-abella-short.pdf}
}

@inproceedings{NigamWOF15,
  author = {Vivek Nigam and Giselle Reis and Leonardo Lima},
  title = {{Towards the Automated Generation of Focused Proof Systems}},
  booktitle = {Proceedings First International Workshop on Focusing, WoF'15},
  pages = {1--6},
  year = {2015},
  doi = {10.4204/EPTCS.197.1},
  url = {http://www.gisellereis.com/papers/gen-focus.pdf}
}

@inproceedings{ChaudhuriR15,
  author = {Kaustuv Chaudhuri and Giselle Reis},
  title = {{An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials}},
  booktitle = {20$^{th}$ International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
  pages = {146--161},
  year = {2015},
  isbn = {978-3-662-48899-7},
  doi = {10.1007/978-3-662-48899-7_11},
  url = {http://www.gisellereis.com/papers/bigraphs.pdf}
}

@inproceedings{Chihani2015,
  author = {Zakaria Chihani and Tomer Libal and Giselle Reis},
  title = {{The Proof Certifier Checkers}},
  booktitle = {24$^{th}$ International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)},
  year = {2015},
  pages = {201--210},
  isbn = {978-3-319-24312-2},
  doi = {10.1007/978-3-319-24312-2_14},
  url = {http://www.gisellereis.com/papers/checkers.pdf}
}

@inproceedings{ReisPXTP15,
  author = {Giselle Reis},
  title = {{Importing SMT and Connection proofs as expansion trees}},
  booktitle = {Fourth Workshop on Proof eXchange for Theorem Proving (PxTP)},
  pages = {3--10},
  year = {2015},
  doi = {10.4204/EPTCS.186.3},
  url = {http://www.gisellereis.com/papers/smt-conn-exp-trees.pdf}
}

@inproceedings{BaazLICS15,
  author = {Matthias Baaz and Alexander Leitsch and Giselle Reis},
  title = {{A Note on the Complexity of Classical and Intuitionistic Proofs}},
  booktitle = {30$^{th}$ Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  pages = {657--666},
  isbn = {978-1-4799-8875-4},
  year = {2015},
  doi = {10.1109/LICS.2015.66},
  url = {http://www.gisellereis.com/papers/lk-lj-compl.pdf}
}

@inproceedings{HetzlIJCAR2014,
  author = {Stefan Hetzl and Alexander Leitsch and Giselle Reis and Janos Tapolczai and Daniel Weller},
  title = {{Introducing Quantified Cuts in Logic with Equality}},
  booktitle = {7$^{th}$ International Joint Conference on Automated Reasoning (IJCAR)},
  pages = {240--254},
  isbn = {978-3-319-08587-6},
  year = {2014},
  doi = {10.1007/978-3-319-08587-6_17},
  url = {http://www.gisellereis.com/papers/cut-intro.pdf}
}

@inproceedings{NigamIJCAR2014,
  author = {Vivek Nigam and Giselle Reis and Leonardo Lima},
  title = {{Quati: An Automated Tool for Proving Permutation Lemmas}},
  booktitle = {7$^{th}$ International Joint Conference on Automated Reasoning (IJCAR 2014)},
  pages = {255--261},
  isbn = {978-3-319-08587-6},
  year = {2014},
  doi = {10.1007/978-3-319-08587-6_18},
  url = {http://www.gisellereis.com/papers/quati.pdf}
}

@inproceedings{NigamTPLP13,
  author = {Vivek Nigam and Giselle Reis and Leonardo Lima},
  title = {{Checking Proof Transformations with ASP}},
  booktitle = {29$^{th}$ International Conference on Logic Programming (ICLP)},
  volume = {13},
  _number = {4-5-Online-Supplement},
  year = {2013},
  url = {http://www.gisellereis.com/papers/proof-trans-asp.pdf}
}

@inproceedings{LeitschCSL12,
  author = {Alexander Leitsch and Giselle Reis and Bruno Woltzenlogel Paleo},
  title = {{Towards CERes in intuitionistic logic}},
  booktitle = {21$^{st}$ EACSL Annual Conference on Computer Science Logic},
  pages = {485--499},
  isbn = {978-3-939897-42-2},
  issn = {1868-8969},
  year = {2012},
  volume = {16},
  doi = {10.4230/LIPIcs.CSL.2012.485},
  url = {http://www.gisellereis.com/papers/lj-ceres-part.pdf}
}

@inproceedings{NigamLSFA10,
  author = {Vivek Nigam and Elaine Pimentel and Giselle Reis},
  title = {{Specifying Proof Systems in Linear Logic with Subexponentials}},
  booktitle = {5$^{th}$ Workshop on Logical and Semantic Frameworks, with Applications (LSFA)},
  volume = {269},
  pages = {109--123},
  year = {2010},
  doi = {10.1016/j.entcs.2011.03.009},
  url = {http://www.gisellereis.com/papers/sellf.pdf}
}

@incollection{ReisEPS1,
  title = {{Intuitionistic Sequent Calculus LJ}},
  author = {Giselle Reis},
  booktitle = {Towards an Encyclopaedia of Proof Systems},
  editor = {Woltzenlogel Paleo, Bruno},
  pages = {5},
  publisher = {College Publications},
  url = {https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf},
  year = {2014},
  edition = {1}
}

@incollection{ReisEPS2,
  title = {{Multi-Conclusion Sequent Calculus LJ'}},
  author = {Giselle Reis and Valeria de Paiva},
  booktitle = {Towards an Encyclopaedia of Proof Systems},
  editor = {Woltzenlogel Paleo, Bruno},
  pages = {8},
  publisher = {College Publications},
  url = {https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf},
  year = {2015},
  edition = {1}
}

@incollection{ReisEPS3,
  title = {{Epsilon-Sound Sequent Calculus LJ$^\star$}},
  author = {Giselle Reis and Bruno Woltzenlogel Paleo},
  booktitle = {An Encyclopaedia of Proof Systems},
  editor = {Woltzenlogel Paleo, Bruno and Reis, Giselle},
  pages = {},
  publisher = {College Publications},
  url = {https://github.com/ProofSystem/Encyclopedia/blob/master/main.pdf},
  year = {2018},
  edition = {2}
}

@proceedings{lsfa2020,
  editor = {Cl\'{a}udia Nalon and Giselle Reis},
  title = {{Proceedings of LSFA 2020, the 15$^{th}$ International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2020)}},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2020},
  doi = {10.1016/j.entcs.2020.08.001}
}

@proceedings{pxtp2019,
  editor = {Haniel Barbosa and Giselle Reis},
  title = {{Proceedings of the Sixth Workshop on Proof eXchange for Theorem Proving (PxTP)}},
  journal = {CoRR},
  year = {2019},
  doi = {10.4204/EPTCS.301}
}

@proceedings{lfmtp2018,
  editor = {Fr{\'{e}}d{\'{e}}ric Blanqui and Giselle Reis},
  title = {{Proceedings of the 13$^{th}$ International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)}},
  journal = {CoRR},
  volume = {abs/1807.01352},
  year = {2018},
  doi = {10.4204/EPTCS.274}
}

@phdthesis{ReisPHD,
  author = {Giselle Reis},
  title = {{Cut-elimination by resolution in intuitionistic logic}},
  type = {PhD thesis},
  school = {Vienna University of Technology},
  year = {2014},
  url = {http://www.gisellereis.com/papers/phd-thesis.pdf}
}

@phdthesis{ReisMSC,
  author = {Giselle Reis},
  title = {{Specification of systems using linear logic with subexponentials (in Portuguese)}},
  type = {MSc thesis},
  school = {Federal University of Minas Gerais},
  year = {2010},
  url = {http://www.gisellereis.com/papers/master-thesis.pdf}
}

@book{EPS,
  title = {{An Encyclopaedia of Proof Systems}},
  editor = {Reis, Giselle and Woltzenlogel Paleo, Bruno},
  publisher = {College Publications},
  address = {London, UK},
  doi = {http://www.collegepublications.co.uk/other/?00028},
  year = {2018},
  edition = {2},
  isbn = {978-1-84890-233-6}
}