6 Search Results for "Balabonski, Thibaut"


Document
A Strong Call-By-Need Calculus

Authors: Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond

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


Abstract
We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a λ-term t admits a normal form n in the λ-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design.

Cite as

Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{balabonski_et_al:LIPIcs.FSCD.2021.9,
  author =	{Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
  title =	{{A Strong Call-By-Need Calculus}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{9:1--9:22},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9},
  URN =		{urn:nbn:de:0030-drops-142477},
  doi =		{10.4230/LIPIcs.FSCD.2021.9},
  annote =	{Keywords: strong reduction, call-by-need, evaluation strategy, normalization}
}
Document
Brave New Idea Paper
Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper)

Authors: Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, its non-deterministic behavior makes it hard to reproduce bugs. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow us to explore a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the right conditions are not triggered. As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allows developers to observe all possible execution paths of a parallel program and debug it interactively. We introduce the concepts of multiverse breakpoints and stepping, which can halt a program in different execution paths, i.e. universes. We apply multiverse debugging to AmbientTalk, an actor-based language, resulting in Voyager, a multiverse debugger implemented on top of the AmbientTalk operational semantics. We provide a proof of non-interference, i.e., we prove that observing the behavior of a program by the debugger does not affect the behavior of that program and vice versa. Multiverse debugging establishes the foundation for debugging non-deterministic programs interactively, which we believe can aid the development of parallel and concurrent systems.

Cite as

Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{torreslopez_et_al:LIPIcs.ECOOP.2019.27,
  author =	{Torres Lopez, Carmen and Gurdeep Singh, Robbert and Marr, Stefan and Gonzalez Boix, Elisa and Scholliers, Christophe},
  title =	{{Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{27:1--27:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.27},
  URN =		{urn:nbn:de:0030-drops-108192},
  doi =		{10.4230/LIPIcs.ECOOP.2019.27},
  annote =	{Keywords: Debugging, Parallelism, Concurrency, Actors, Formal Semantics}
}
Document
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.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
The Silently Shifting Semicolon

Authors: Daniel Marino, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, and Abhayendra Singh

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)


Abstract
Memory consistency models for modern concurrent languages have largely been designed from a system-centric point of view that protects, at all costs, optimizations that were originally designed for sequential programs. The result is a situation that, when viewed from a programmer's standpoint, borders on absurd. We illustrate this unfortunate situation with a brief fable and then examine the opportunities to right our path.

Cite as

Daniel Marino, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, and Abhayendra Singh. The Silently Shifting Semicolon. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 177-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{marino_et_al:LIPIcs.SNAPL.2015.177,
  author =	{Marino, Daniel and Millstein, Todd and Musuvathi, Madanlal and Narayanasamy, Satish and Singh, Abhayendra},
  title =	{{The Silently Shifting Semicolon}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{177--189},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.177},
  URN =		{urn:nbn:de:0030-drops-50259},
  doi =		{10.4230/LIPIcs.SNAPL.2015.177},
  annote =	{Keywords: memory consistency models; sequential consistency; safe programming languages; data races}
}
Document
A Few Lessons from the Mezzo Project

Authors: Francois Pottier and Jonathan Protzenko

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)


Abstract
With Mezzo, we set out to design a new, better programming language. In this modest document, we recount our adventure: what worked, and what did not; the decisions that appear in hindsight to have been good, and the design mistakes that cost us; the things that we are happy with in the end, and the frustrating aspects we wish we had handled better.

Cite as

Francois Pottier and Jonathan Protzenko. A Few Lessons from the Mezzo Project. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 221-237, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{pottier_et_al:LIPIcs.SNAPL.2015.221,
  author =	{Pottier, Francois and Protzenko, Jonathan},
  title =	{{A Few Lessons from the Mezzo Project}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{221--237},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.221},
  URN =		{urn:nbn:de:0030-drops-50281},
  doi =		{10.4230/LIPIcs.SNAPL.2015.221},
  annote =	{Keywords: static type systems, side effects, aliasing, ownership}
}
Document
Axiomatic Sharing-via-Labelling

Authors: Thibaut Balabonski

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)


Abstract
A judicious use of labelled terms makes it possible to bring together the simplicity of term rewriting and the sharing power of graph rewriting: this has been known for twenty years in the particular case of orthogonal first-order systems. The present paper introduces a concise and easily usable axiomatic presentation of sharing-via-labelling techniques that applies to higher-order term rewriting as well as to non-orthogonal term rewriting. This provides a general framework for the sharing of subterms and keeps the formalism as simple as term rewriting.

Cite as

Thibaut Balabonski. Axiomatic Sharing-via-Labelling. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 85-100, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{balabonski:LIPIcs.RTA.2012.85,
  author =	{Balabonski, Thibaut},
  title =	{{Axiomatic Sharing-via-Labelling}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{85--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.85},
  URN =		{urn:nbn:de:0030-drops-34868},
  doi =		{10.4230/LIPIcs.RTA.2012.85},
  annote =	{Keywords: Sharing, Abstract term rewriting, Graphs, Higher order, Non-orthogonality}
}
  • Refine by Author
  • 2 Balabonski, Thibaut
  • 1 Bucciarelli, Antonio
  • 1 Gonzalez Boix, Elisa
  • 1 Gurdeep Singh, Robbert
  • 1 Kesner, Delia
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Concurrent programming languages
  • 1 Software and its engineering → Software testing and debugging
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 1 Abstract term rewriting
  • 1 Actors
  • 1 Concurrency
  • 1 Debugging
  • 1 Formal Semantics
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2015
  • 1 2012
  • 1 2019
  • 1 2021

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