Search Results

Documents authored by Chaudhuri, Kaustuv

Document
DOI: 10.4230/LIPIcs.FSCD.2016.16
Modular Focused Proof Systems for Intuitionistic Modal Logics

Authors: Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Focusing is a general technique for syntactically compartmentalizing the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing is usually specified as a restriction of the sequent calculus, the technique has not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some of the logics of the modal cube. We have recently extended the focusing technique to classical nested sequents, a generalization of ordinary sequents. In this work we further extend focusing to intuitionistic nested sequents, which can capture all the logics of the intuitionistic S5 cube in a modular fashion. We present an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.
Cite as

Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.FSCD.2016.16,
  author =	{Chaudhuri, Kaustuv and Marin, Sonia and Stra{\ss}burger, Lutz},
  title =	{{Modular Focused Proof Systems for Intuitionistic Modal Logics}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.16},
  URN =		{urn:nbn:de:0030-drops-59947},
  doi =		{10.4230/LIPIcs.FSCD.2016.16},
  annote =	{Keywords: intuitionistic modal logic, focusing, proof search, cut elimination, nested sequents}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.332
A Proof-theoretic Characterization of Independence in Type Theory

Authors: Yuting Wang and Kaustuv Chaudhuri

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
For lambda-terms constructed freely from a type signature in a type theory such as LF, there is a simple inductive subordination relation that is used to control type-formation. There is a related—but not precisely complementary—notion of independence that asserts that the inhabitants of the function space tau_1 --> tau_2 depend vacuously on their arguments. Independence has many practical reasoning applications in logical frameworks, such as pruning variable dependencies or transporting theorems and proofs between type signatures. However, independence is usually not given a formal interpretation. Instead, it is generally implemented in an ad hoc and uncertified fashion. We propose a formal definition of independence and give a proof-theoretic characterization of it by: (1) representing the inference rules of a given type theory and a closed type signature as a theory of intuitionistic predicate logic, (2) showing that typing derivations in this signature are adequately represented by a focused sequent calculus for this logic, and (3) defining independence in terms of strengthening for intuitionistic sequents. This scheme is then formalized in a meta-logic, called G, that can represent the sequent calculus as an inductive definition, so the relevant strengthening lemmas can be given explicit inductive proofs. We present an algorithm for automatically deriving the strengthening lemmas and their proofs in G.
Cite as

Yuting Wang and Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 332-346, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.TLCA.2015.332,
  author =	{Wang, Yuting and Chaudhuri, Kaustuv},
  title =	{{A Proof-theoretic Characterization of Independence in Type Theory}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{332--346},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.332},
  URN =		{urn:nbn:de:0030-drops-51736},
  doi =		{10.4230/LIPIcs.TLCA.2015.332},
  annote =	{Keywords: subordination; independence; sequent calculus; focusing; strengthening}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.557
A Two-Level Logic Approach to Reasoning About Typed Specification Languages

Authors: Mary Southern and Kaustuv Chaudhuri

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.
Cite as

Mary Southern and Kaustuv Chaudhuri. A Two-Level Logic Approach to Reasoning About Typed Specification Languages. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 557-569, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{southern_et_al:LIPIcs.FSTTCS.2014.557,
  author =	{Southern, Mary and Chaudhuri, Kaustuv},
  title =	{{A Two-Level Logic Approach to Reasoning About Typed Specification Languages}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{557--569},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.557},
  URN =		{urn:nbn:de:0030-drops-48716},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.557},
  annote =	{Keywords: Abella theorem prover, two-level logic, typed specification languages}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2013.150
A Hybrid Linear Logic for Constrained Transition Systems

Authors: Joëlle Despeyroux and Kaustuv Chaudhuri

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus.
Cite as

Joëlle Despeyroux and Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 150-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{despeyroux_et_al:LIPIcs.TYPES.2013.150,
  author =	{Despeyroux, Jo\"{e}lle and Chaudhuri, Kaustuv},
  title =	{{A Hybrid Linear Logic for Constrained Transition Systems}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{150--168},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.150},
  URN =		{urn:nbn:de:0030-drops-46302},
  doi =		{10.4230/LIPIcs.TYPES.2013.150},
  annote =	{Keywords: Linear logic, hybrid logic, stochastic pi-calculus, focusing, adequacy}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.183
A Systematic Approach to Canonicity in the Classical Sequent Calculus

Authors: Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
The sequent calculus is often criticized for requiring proofs to contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps-such as instantiating a block of quantifiers-by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity: proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings, and atomic flows are examples of such revolutionary formalisms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means of abstracting away the details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that make the foci as parallel as possible are canonical. Moreover, such proofs are isomorphic to expansion proofs - a well known, minimalistic, and parallel generalization of Herbrand disjunctions - for classical first-order logic. This technique is a systematic way to recover the desired essence of any sequent proof without abandoning the sequent calculus.
Cite as

Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 183-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2012.183,
  author =	{Chaudhuri, Kaustuv and Hetzl, Stefan and Miller, Dale},
  title =	{{A Systematic Approach to Canonicity in the Classical Sequent Calculus}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{183--197},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.183},
  URN =		{urn:nbn:de:0030-drops-36723},
  doi =		{10.4230/LIPIcs.CSL.2012.183},
  annote =	{Keywords: Sequent Calculus, Canonicity, Classical Logic, Expansion Trees}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.159
The Focused Calculus of Structures

Authors: Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
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.
Cite as

Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The Focused Calculus of Structures. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 159-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2011.159,
  author =	{Chaudhuri, Kaustuv and Guenot, Nicolas and Stra{\ss}burger, Lutz},
  title =	{{The Focused Calculus of Structures}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{159--173},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.159},
  URN =		{urn:nbn:de:0030-drops-32297},
  doi =		{10.4230/LIPIcs.CSL.2011.159},
  annote =	{Keywords: focusing, polarity, calculus of structures, linear logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact