Author name cluster

Nicolas Guenot

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

LFMTP Workshop 2015 Workshop Paper

Sequent Calculus and Equational Programming

Nicolas Guenot
Daniel Gustafsson

Proof assistants and programming languages based on type theories usually come in two flavours: one is based on the standard natural deduction presentation of type theory and involves eliminators, while the other provides a syntax in equational style. We show here that the equational approach corresponds to the use of a focused presentation of a type theory expressed as a sequent calculus. A typed functional language is presented, based on a sequent calculus, that we relate to the syntax and internal language of Agda. In particular, we discuss the use of patterns and case splittings, as well as rules implementing inductive reasoning and dependent products and sums.

Details DOI

LFMTP Workshop 2014 Conference Paper

Hybrid Extensions in a Logical Framework

Taus Brock-Nannestad
Nicolas Guenot
Agata Murawska
Carsten Schürmann 0001

We discuss the extension of the LF logical framework with operators for manipulating worlds, as found in hybrid logics or in the HLF framework. To overcome the restrictions of HLF, we present a more general approach to worlds in LF, where the structure of worlds can be described in an explicit way. We give a canonical presentation for this system and discuss the encoding of logical systems, beyond the limited scope of linear logic that formed the main goal of HLF.

Details

CSL Conference 2011 Conference Paper

The Focused Calculus of Structures

Kaustuv Chaudhuri
Nicolas Guenot
Lutz Straßburger

The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited both for the search and for the representation of sequent proofs. The calculus of structures is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but standard presentations of this calculus are too permissive, allowing too many proofs. In order to make it more amenable to proof search, we transplant the focusing theorem from the sequent calculus to the calculus of structures. The key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof.

Details