13 citations · 21 across the 10 of their papers we have counts for
10 papers · 1 filter
Facilitating Meta-Theory Reasoning (Invited Paper)
Giselle Reis
Structural proof theory is praised for being a symbolic approach to reasoning and proofs, in which one can define schemas for reasoning steps and manipulate proofs as a mathematica…
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
Laila El-Beheiry, Giselle Reis, Ammar Karkour
Formally reasoning about functional programs is supposed to be straightforward and elegant, however, it is not typically done as a matter of course. Reasoning in a proof assistant…
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving
Giselle Reis, Haniel Barbosa
This volume of EPTCS contains the proceedings of the Sixth Workshop on Proof Exchange for Theorem Proving (PxTP 2019), held on 26 August 2019 as part of the CADE-27 conference in N…
The ILLTP Library for Intuitionistic Linear Logic
Carlos Olarte, Valeria de Paiva, Elaine Pimentel +1
Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such…
Formalization of Automated Trading Systems in a Concurrent Linear Framework
Iliano Cervesato, Sharjeel Khan, Giselle Reis +1
We present a declarative and modular specification of an automated trading system (ATS) in the concurrent linear framework CLF. We implemented it in Celf, a CLF type checker which…
Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Frédéric Blanqui, Giselle Reis
This volume contains a selection of papers presented at LFMTP 2018, the 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on J…
Towards the Automated Generation of Focused Proof Systems
Vivek Nigam, Giselle Reis, Leonardo Lima
This paper tackles the problem of formulating and proving the completeness of focused-like proof systems in an automated fashion. Focusing is a discipline on proofs which structure…
Importing SMT and Connection proofs as expansion trees
Giselle Reis
Different automated theorem provers reason in various deductive systems and, thus, produce proof objects which are in general not compatible. To understand and analyze these object…
Introducing Quantified Cuts in Logic with Equality
Stefan Hetzl, Alexander Leitsch, Giselle Reis +2
Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of…
Algorithmic Introduction of Quantified Cuts
Stefan Hetzl, Alexander Leitsch, Giselle Reis +1
We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computign a compressed representation of the terms pres…