DROPS

Volume

LIPIcs, Volume 23

Computer Science Logic 2013 (CSL 2013)

CSL 2013, September 2-5, 2013, Torino, Italy

Editors: Simona Ronchi Della Rocca

Document

DOI: 10.4230/LIPIcs.FSCD.2023.29

A Quantitative Version of Simple Types

Authors: Daniele Pautasso and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

This work introduces a quantitative version of the simple type assignment system, starting from a suitable restriction of non-idempotent intersection types. The resulting system is decidable and has the same typability power as the simple type system; thus, assigning types to terms supplies the very same qualitative information given by simple types, but at the same time can provide some interesting quantitative information. It is well known that typability for simple types is equivalent to unification; we prove a similar result for the newly introduced system. More precisely, we show that typability is equivalent to a unification problem which is a non-trivial extension of the classical one: in addition to unification rules, our typing algorithm makes use of an expansion operation that increases the cardinality of multisets whenever needed.

Cite as

Daniele Pautasso and Simona Ronchi Della Rocca. A Quantitative Version of Simple Types. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{pautasso_et_al:LIPIcs.FSCD.2023.29,
  author =	{Pautasso, Daniele and Ronchi Della Rocca, Simona},
  title =	{{A Quantitative Version of Simple Types}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{29:1--29:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.29},
  URN =		{urn:nbn:de:0030-drops-180137},
  doi =		{10.4230/LIPIcs.FSCD.2023.29},
  annote =	{Keywords: \lambda-calculus, intersection types, unification}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2022.36

An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus

Authors: Luca Ciccone and Luca Padovani

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract

Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of μMALL^∞, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of πLIN, a variant of the linear π-calculus with (co)recursive types into which binary and (some) multiparty sessions can be encoded. As a result we obtain a behavioral type system for πLIN (and indirectly for session calculi through their encoding into πLIN) that ensures fair termination: although well-typed processes may engage in arbitrarily long interactions, they are fairly guaranteed to eventually perform all pending actions.

Cite as

Luca Ciccone and Luca Padovani. An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ciccone_et_al:LIPIcs.CONCUR.2022.36,
  author =	{Ciccone, Luca and Padovani, Luca},
  title =	{{An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear \pi-Calculus}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.36},
  URN =		{urn:nbn:de:0030-drops-170990},
  doi =		{10.4230/LIPIcs.CONCUR.2022.36},
  annote =	{Keywords: Linear \pi-calculus, Linear Logic, Fixed Points, Fair Termination}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2021.7

Call-By-Value, Again!

Authors: Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.

Cite as

Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-By-Value, Again!. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kerinec_et_al:LIPIcs.FSCD.2021.7,
  author =	{Kerinec, Axel and Manzonetto, Giulio and Ronchi Della Rocca, Simona},
  title =	{{Call-By-Value, Again!}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.7},
  URN =		{urn:nbn:de:0030-drops-142458},
  doi =		{10.4230/LIPIcs.FSCD.2021.7},
  annote =	{Keywords: \lambda-calculus, call-by-value, intersection types, solvability, inhabitation}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2019.3

A Quantitative Understanding of Pattern Matching

Authors: Sandra Alves, Delia Kesner, and Daniel Ventura

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract

This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E, for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [Antonio Bucciarelli et al., 2015], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [Antonio Bucciarelli et al., 2015], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [Antonio Bucciarelli et al., 2015], which turn out to be an essential quantitative tool because they remove the confusion between "being a pair" and "being duplicable". Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors.

Cite as

Sandra Alves, Delia Kesner, and Daniel Ventura. A Quantitative Understanding of Pattern Matching. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 3:1-3:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{alves_et_al:LIPIcs.TYPES.2019.3,
  author =	{Alves, Sandra and Kesner, Delia and Ventura, Daniel},
  title =	{{A Quantitative Understanding of Pattern Matching}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{3:1--3:36},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.3},
  URN =		{urn:nbn:de:0030-drops-130672},
  doi =		{10.4230/LIPIcs.TYPES.2019.3},
  annote =	{Keywords: Intersection Types, Pattern Matching, Exact Bounds}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2020.1

Solvability in a Probabilistic Setting (Invited Talk)

Authors: Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

The notion of solvability, crucial in the λ-calculus, is conservatively extended to a probabilistic setting, and a complete characterization of it is given. The employed technical tool is a type assignment system, based on non-idempotent intersection types, whose typable terms turn out to be precisely the terms which are solvable with nonnull probability. We also supply an operational characterization of solvable terms, through the notion of head normal form, and a denotational model of Λ_⊕, itself induced by the type system, which equates all the unsolvable terms.

Cite as

Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian. Solvability in a Probabilistic Setting (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ronchidellarocca_et_al:LIPIcs.FSCD.2020.1,
  author =	{Ronchi Della Rocca, Simona and Dal Lago, Ugo and Faggian, Claudia},
  title =	{{Solvability in a Probabilistic Setting}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{1:1--1:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.1},
  URN =		{urn:nbn:de:0030-drops-123237},
  doi =		{10.4230/LIPIcs.FSCD.2020.1},
  annote =	{Keywords: Probabilistic Computation, Lambda Calculus, Solvability, Intersection Types}
}

Document

Invited Paper

DOI: 10.4230/LIPIcs.TYPES.2016.2

Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper)

Authors: Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract

This is a short survey of the use of intersection types for reasoning in a finitary way about terms interpretations in various models of lambda-calculus.

Cite as

Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 2:1-2:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ronchidellarocca:LIPIcs.TYPES.2016.2,
  author =	{Ronchi Della Rocca, Simona},
  title =	{{Intersection Types and Denotational Semantics: An Extended Abstract}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{2:1--2:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.2},
  URN =		{urn:nbn:de:0030-drops-98614},
  doi =		{10.4230/LIPIcs.TYPES.2016.2},
  annote =	{Keywords: Lambda-calculus, Lambda-models, Intersection types}
}

Document

DOI: 10.4230/LIPIcs.CSL.2015.xv

The Ackermann Award 2015

Authors: Anuj Dawar, Dexter Kozen, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.

Cite as

Anuj Dawar, Dexter Kozen, and Simona Ronchi Della Rocca. The Ackermann Award 2015. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 15-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2015.xv,
  author =	{Dawar, Anuj and Kozen, Dexter and Ronchi Della Rocca, Simona},
  title =	{{The Ackermann Award 2015}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{15--18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.xv},
  URN =		{urn:nbn:de:0030-drops-54470},
  doi =		{10.4230/LIPIcs.CSL.2015.xv},
  annote =	{Keywords: Ackermann Award}
}

Document

DOI: 10.4230/LIPIcs.TLCA.2015.123

Observability for Pair Pattern Calculi

Authors: Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca

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

Abstract

Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which — together with typability — allows to obtain a full characterization of observability.

Cite as

Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 123-137, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.TLCA.2015.123,
  author =	{Bucciarelli, Antonio and Kesner, Delia and Ronchi Della Rocca, Simona},
  title =	{{Observability for Pair Pattern Calculi}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{123--137},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.123},
  URN =		{urn:nbn:de:0030-drops-51596},
  doi =		{10.4230/LIPIcs.TLCA.2015.123},
  annote =	{Keywords: solvability, pattern calculi, intersection types, inhabitation}
}

Document

DOI: 10.4230/LIPIcs.TLCA.2015.211

Standardization of a Call-By-Value Lambda-Calculus

Authors: Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca

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

Abstract

We study an extension of Plotkin's call-by-value lambda-calculus by means of two commutation rules (sigma-reductions). Recently, it has been proved that this extended calculus provides elegant characterizations of many semantic properties, as for example solvability. We prove a standardization theorem for this calculus by generalizing Takahashi's approach of parallel reductions. The standardization property allows us to prove that our calculus is conservative with respect to the Plotkin's one. In particular, we show that the notion of solvability for this calculus coincides with that for Plotkin's call-by-value lambda-calculus.

Cite as

Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 211-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.TLCA.2015.211,
  author =	{Guerrieri, Giulio and Paolini, Luca and Ronchi Della Rocca, Simona},
  title =	{{Standardization of a Call-By-Value Lambda-Calculus}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{211--225},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.211},
  URN =		{urn:nbn:de:0030-drops-51655},
  doi =		{10.4230/LIPIcs.TLCA.2015.211},
  annote =	{Keywords: standardization,sequentialization,lambda-calculus,sigma-reduction,par- allel reduction, call-by-value, head reduction, internal reduction, solvability}
}

Document

Complete Volume

DOI: 10.4230/LIPIcs.CSL.2013

LIPIcs, Volume 23, CSL'13, Complete Volume

Authors: Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

LIPIcs, Volume 23, CSL'13, Complete Volume

Cite as

Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{ronchidellarocca:LIPIcs.CSL.2013,
  title =	{{LIPIcs, Volume 23, CSL'13, Complete Volume}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013},
  URN =		{urn:nbn:de:0030-drops-42618},
  doi =		{10.4230/LIPIcs.CSL.2013},
  annote =	{Keywords: Conference Proceedings, Theory of Computation, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory Languages Constructs and Features, Knowledge Representations Formalisms and Methods}
}

Document

Front Matter

DOI: 10.4230/LIPIcs.CSL.2013.i

Frontmatter, Table of Contents, Preface, Conference Organization

Authors: Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

Frontmatter, Table of Contents, Preface, Conference Organization

Cite as

Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{ronchidellarocca:LIPIcs.CSL.2013.i,
  author =	{Ronchi Della Rocca, Simona},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{i--xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.i},
  URN =		{urn:nbn:de:0030-drops-41821},
  doi =		{10.4230/LIPIcs.CSL.2013.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}

Document

DOI: 10.4230/LIPIcs.CSL.2013.1

The Ackermann Award 2013

Authors: Anuj Dawar, Thomas A. Henzinger, and Damian Niwiński

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

Report on the Ackermann Award 2013.

Cite as

Anuj Dawar, Thomas A. Henzinger, and Damian Niwiński. The Ackermann Award 2013. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2013.1,
  author =	{Dawar, Anuj and Henzinger, Thomas A. and Niwi\'{n}ski, Damian},
  title =	{{The Ackermann Award 2013}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{1--4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.1},
  URN =		{urn:nbn:de:0030-drops-41837},
  doi =		{10.4230/LIPIcs.CSL.2013.1},
  annote =	{Keywords: Ackermann award}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.CSL.2013.5

Res Publica: The Universal Model of Computation (Invited Talk)

Authors: Nachum Dershowitz

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

We proffer a model of computation that encompasses a broad variety of contemporary generic models, such as cellular automata---including dynamic ones, and abstract state machines---incorporating, as they do, interaction and parallelism. We ponder what it means for such an intertwined system to be effective and note that the suggested framework is ideal for representing continuous-time and asynchronous systems.

Cite as

Nachum Dershowitz. Res Publica: The Universal Model of Computation (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 5-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{dershowitz:LIPIcs.CSL.2013.5,
  author =	{Dershowitz, Nachum},
  title =	{{Res Publica: The Universal Model of Computation}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{5--10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.5},
  URN =		{urn:nbn:de:0030-drops-41844},
  doi =		{10.4230/LIPIcs.CSL.2013.5},
  annote =	{Keywords: Models of computation, cellular automata, abstract state machines, causal dynamics, interaction}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.CSL.2013.11

Three lightings of logic (Invited Talk)

Authors: Jean-Yves Girard

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

Whether we deal with foundations or computation, logic relates questions and answers, typically formulas and proofs: a very entangled relation due to the abuse of presuppositions. In order to analyse syntax, we should step out from language, which is quite impossible. However, it is enough to step out from meaning: this is why our first lighting of logic is that of answers: it is possible to deal with them as meaningless artifacts assuming two basic states, implicit and explicit. The process of explicitation (a.k.a. normalisation, execution), which aims at making explicit what is only implicit, is fundamentally hazardous. The second light is that of questions whose choice involves a formatting ensuring the convergence of explicitation, i.e., the existence of "normal forms". This formatting can be seen as the emergence of meaning. It is indeed a necessary nuisance; either too laxist or too coercitive, there is no just format. Logic should avoid the pitfall of Prussian, axiomatic, formats by trying to understand which deontic dialogue is hidden behind logical restrictions. The third lighting, certainty deals with the adequation between answers and questions: how do we know that an answer actually matches a question? Apodictic certainty -- beyond a reasonable doubt -- is out of reach: we can only hope for epidictic, i.e., limited, reasonable, certainty. Under the second light (questions), we see that the format is made of two opposite parts, namely rights and duties, and that logical deduction relies on a strict balance between these two opposite terms, expressed by the identity group "A is A and conversely". The issue of certainty thus becomes the interrogation: "Can we afford the rights of our duties?"

Cite as

Jean-Yves Girard. Three lightings of logic (Invited Talk). In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 11-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{girard:LIPIcs.CSL.2013.11,
  author =	{Girard, Jean-Yves},
  title =	{{Three lightings of logic}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{11--23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.11},
  URN =		{urn:nbn:de:0030-drops-41852},
  doi =		{10.4230/LIPIcs.CSL.2013.11},
  annote =	{Keywords: Proof theory}
}

54 Search Results for "Ronchi Della Rocca, Simona"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message