7 Search Results for "Bach Poulsen, Casper"

Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.47
Defining Name Accessibility Using Scope Graphs

Authors: Aron Zwaan and Casper Bach Poulsen

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility. We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages. Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately.
Cite as

Aron Zwaan and Casper Bach Poulsen. Defining Name Accessibility Using Scope Graphs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 47:1-47:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zwaan_et_al:LIPIcs.ECOOP.2024.47,
  author =	{Zwaan, Aron and Bach Poulsen, Casper},
  title =	{{Defining Name Accessibility Using Scope Graphs}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{47:1--47:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.47},
  URN =		{urn:nbn:de:0030-drops-208961},
  doi =		{10.4230/LIPIcs.ECOOP.2024.47},
  annote =	{Keywords: access modifier, visibility, scope graph, name resolution}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.27
Defining Name Accessibility Using Scope Graphs (Artifact)

Authors: Aron Zwaan and Casper Bach Poulsen

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility. We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages. Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately.
Cite as

Aron Zwaan and Casper Bach Poulsen. Defining Name Accessibility Using Scope Graphs (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 27:1-27:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{zwaan_et_al:DARTS.10.2.27,
  author =	{Zwaan, Aron and Bach Poulsen, Casper},
  title =	{{Defining Name Accessibility Using Scope Graphs (Artifact)}},
  pages =	{27:1--27:3},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Zwaan, Aron and Bach Poulsen, Casper},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.27},
  URN =		{urn:nbn:de:0030-drops-209258},
  doi =		{10.4230/DARTS.10.2.27},
  annote =	{Keywords: access modifier, visibility, scope graph, name resolution}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.2
Renamingless Capture-Avoiding Substitution for Definitional Interpreters

Authors: Casper Bach Poulsen

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Substitution is a common and popular approach to implementing name binding in definitional interpreters. A common pitfall of implementing substitution functions is variable capture. The traditional approach to avoiding variable capture is to rename variables. However, traditional renaming makes for an inefficient interpretation strategy. Furthermore, for applications where partially-interpreted terms are user facing it can be confusing if names in uninterpreted parts of the program have been changed. In this paper we explore two techniques for implementing capture avoiding substitution in definitional interpreters to avoid renaming.
Cite as

Casper Bach Poulsen. Renamingless Capture-Avoiding Substitution for Definitional Interpreters. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bachpoulsen:OASIcs.EVCS.2023.2,
  author =	{Bach Poulsen, Casper},
  title =	{{Renamingless Capture-Avoiding Substitution for Definitional Interpreters}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{2:1--2:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.2},
  URN =		{urn:nbn:de:0030-drops-177728},
  doi =		{10.4230/OASIcs.EVCS.2023.2},
  annote =	{Keywords: Capture-avoiding substitution, lambda calculus, definitional interpreter}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.32
Scope Graphs: The Story so Far

Authors: Aron Zwaan and Hendrik van Antwerpen

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Static name binding (i.e., associating references with appropriate declarations) is an essential aspect of programming languages. However, it is usually treated in an unprincipled manner, often leaving a gap between formalization and implementation. The scope graph formalism mitigates these deficiencies by providing a well-defined, first-class, language-parametric representation of name binding. Scope graphs serve as a foundation for deriving type checkers from declarative type system specifications, reasoning about type soundness, and implementing editor services and refactorings. In this paper we present an overview of scope graphs, and, using examples, show how the ideas and notation of the formalism have evolved. We also briefly discuss follow-up research beyond type checking, and evaluate the formalism.
Cite as

Aron Zwaan and Hendrik van Antwerpen. Scope Graphs: The Story so Far. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 32:1-32:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{zwaan_et_al:OASIcs.EVCS.2023.32,
  author =	{Zwaan, Aron and van Antwerpen, Hendrik},
  title =	{{Scope Graphs: The Story so Far}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{32:1--32:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.32},
  URN =		{urn:nbn:de:0030-drops-178020},
  doi =		{10.4230/OASIcs.EVCS.2023.32},
  annote =	{Keywords: scope graph, name binding, reference resolution, type system, static semantics}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.20
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics

Authors: Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Semantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper, we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework for name resolution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection.
Cite as

Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 20:1-20:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bachpoulsen_et_al:LIPIcs.ECOOP.2016.20,
  author =	{Bach Poulsen, Casper and N\'{e}ron, Pierre and Tolmach, Andrew and Visser, Eelco},
  title =	{{Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{20:1--20:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.20},
  URN =		{urn:nbn:de:0030-drops-61140},
  doi =		{10.4230/LIPIcs.ECOOP.2016.20},
  annote =	{Keywords: Dynamic semantics, scope graphs, memory layout, type soundness, operational semantics}
}
Document
DOI: 10.4230/DARTS.2.1.10
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)

Authors: Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Our paper introduces a systematic approach to the alignment of names in the static structure of a program, and memory layout and access during its execution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection. This Coq artifact showcases how our uniform model for memory layout in dynamic semantics provides structure to type soundness proofs. The artifact contains type soundness proofs mechanized in Coq for (supersets of) all languages in the paper. The type soundness proofs rely on a language-independent framework formalizing scope graphs and frame heaps.
Cite as

Casper Bach Poulsen, Pierre Néron, Andrew Tolmach, and Eelco Visser. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bachpoulsen_et_al:DARTS.2.1.10,
  author =	{Bach Poulsen, Casper and Néron, Pierre and Tolmach, Andrew and Visser, Eelco},
  title =	{{Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)}},
  pages =	{10:1--10:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Bach Poulsen, Casper and Néron, Pierre and Tolmach, Andrew and Visser, Eelco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.10},
  URN =		{urn:nbn:de:0030-drops-61314},
  doi =		{10.4230/DARTS.2.1.10},
  annote =	{Keywords: Dynamic semantics, scope graphs, memory layout, type soundness, operational semantics}
}
  • Refine by Type
  • 7 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2024
  • 2 2023
  • 2 2016

  • Refine by Author
  • 5 Bach Poulsen, Casper
  • 3 Zwaan, Aron
  • 2 Tolmach, Andrew
  • 2 Visser, Eelco
  • 1 Li, Elaine
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 2 OASIcs
  • 2 DARTS

  • Refine by Classification
  • 2 Software and its engineering → Compilers
  • 2 Software and its engineering → Language features
  • 2 Theory of computation → Program constructs
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 3 scope graph
  • 2 Dynamic semantics
  • 2 access modifier
  • 2 memory layout
  • 2 name resolution
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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