DROPS

Document

Scalable Handling of Effects (Dagstuhl Seminar 21292)

Authors: Danel Ahman, Amal Ahmed, Sam Lindley, and Andreas Rossberg

Published in: Dagstuhl Reports, Volume 11, Issue 6 (2021)

Abstract

Built on solid mathematical foundations, effect handlers offer a uniform and elegant approach to programming with user-defined computational effects. They subsume many widely used programming concepts and abstractions, such as actors, async/await, backtracking, coroutines, generators/iterators, and probabilistic programming. As such, they allow language implementers to target a single implementation of effect handlers, freeing language implementers from having to maintain separate ad hoc implementations of each of the features listed above. Due to their wide applicability, effect handlers are enjoying growing interest in academia and industry. For instance, several effect handler oriented research languages are under active development (such as Eff, Frank, and Koka), as are effect handler libraries for mainstream languages (such as C and Java), effect handlers are seeing increasing use in probabilistic programming tools (such as Uber’s Pyro), and proposals are in the pipeline to include them natively in low-level languages (such as WebAssembly). Effect handlers are also a key part of Multicore OCaml, which incorporates an efficient implementation of them for uniformly expressing user-definable concurrency models in the language. However, enabling effect handlers to scale requires tackling some hard problems, both in theory and in practice. Inspired by experience of developing, programming with, and reasoning about effect handlers in practice, we identify five key problem areas to be addressed at this Dagstuhl Seminar in order to enable effect handlers to scale: Safety, Modularity, Interoperability, Legibility, and Efficiency. In particular, we seek answers to the following questions: - How can we enforce safe interaction between effect handler programs and external resources? - How can we enable modular use of effect handlers for programming in the large? - How can we support interoperable effect handler programs written in different languages? - How can we write legible effect handler programs in a style accessible to mainstream programmers? - How can we generate efficient code from effect handler programs?

Cite as

Danel Ahman, Amal Ahmed, Sam Lindley, and Andreas Rossberg. Scalable Handling of Effects (Dagstuhl Seminar 21292). In Dagstuhl Reports, Volume 11, Issue 6, pp. 54-81, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{ahman_et_al:DagRep.11.6.54,
  author =	{Ahman, Danel and Ahmed, Amal and Lindley, Sam and Rossberg, Andreas},
  title =	{{Scalable Handling of Effects (Dagstuhl Seminar 21292)}},
  pages =	{54--81},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2021},
  volume =	{11},
  number =	{6},
  editor =	{Ahman, Danel and Ahmed, Amal and Lindley, Sam and Rossberg, Andreas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.6.54},
  URN =		{urn:nbn:de:0030-drops-155800},
  doi =		{10.4230/DagRep.11.6.54},
  annote =	{Keywords: continuations, Effect handlers, Wasm}
}

Document

SCICO Journal-first

DOI: 10.4230/LIPIcs.ECOOP.2020.33

Abstracting Gradual References (SCICO Journal-first)

Authors: Matías Toro and Éric Tanter

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

Gradual typing is an effective approach to integrate static and dynamic typing, which supports the smooth transition between both extremes via the (programmer-controlled) precision of type annotations [Jeremy Siek and Walid Taha, 2006; Siek et al., 2015]. Imprecision is normally introduced via the unknown type ?, e.g. function type Int → Bool is more precise than ? → ?, and both more precise than ?. Gradual typing relates types of different precision using consistent type relations, such as type consistency (resp. consistent subtyping), the gradual counterpart of type equality (resp. subtyping). For instance, ? → Int is consistent with Bool → ?. This approach has been applied in a number of settings, such as objects [Jeremy Siek and Walid Taha, 2007], subtyping [Jeremy Siek and Walid Taha, 2007; Ronald Garcia et al., 2016], effects [Bañados Schwerter et al., 2014; Bañados Schwerter et al., 2016], ownership [Ilya Sergey and Dave Clarke, 2012], typestates [Roger Wolff et al., 2011; Ronald Garcia et al., 2014], information-flow typing [Tim Disney and Cormac Flanagan, 2011; Luminous Fennell and Peter Thiemann, 2013; Matías Toro et al., 2018], session types [Igarashi et al., 2017], refinements [Nico Lehmann and {É}ric Tanter, 2017], set-theoretic types [Castagna and Lanvin, 2017], Hoare logic [Johannes Bader et al., 2018], parametric polymorphism [Amal Ahmed et al., 2011; Ahmed et al., 2017; Ina and Igarashi, 2011; Igarashi et al., 2017; Ningning Xie et al., 2018; Matías Toro et al., 2019], and references [Jeremy Siek and Walid Taha, 2006; Herman et al., 2010; Siek et al., 2015]. In particular, gradual typing for mutable references has seen the elaboration of various possible semantics: invariant references [Jeremy Siek and Walid Taha, 2006], guarded references [Herman et al., 2010], monotonic references [Siek et al., 2015], and permissive references [Siek et al., 2015]. Invariant references are a form of references where reference types are invariant with respect to type consistency. Guarded references admit variance thanks to systematic runtime checks on reference reads and writes; the runtime type of an allocated cell never changes during execution. Guarded references have been formulated in a space-efficient coercion calculus, which ensures that gradual programs do not accumulate unbounded pending checks during execution. Hereafter, we refer to this language as HCC. Monotonic references favor efficiency over flexibility by only allowing reference cells to vary towards more precise types. This allows reference operations in statically-typed regions to safely proceed without any runtime checks. Permissive references are the most flexible approach, in which reference cells can be initialized and updated to any value of any type at any time. These four developments reflect different design decisions with respect to gradual references: is the reference type constructor variant under consistency? Can the programmer specify a precise bound on the static type of a reference, and hence on the corresponding heap cell type? Can the heap cell type evolve its precision at runtime, and if yes, how? There is obviously no absolute answer to these questions, as they reflect different tradeoffs such as in efficiency and precision. This work explores the semantics that results from the application of a systematic methodology to gradualize static type systems. Currently we can find in the literature two methodologies to gradualize statically-typed languages: Abstracting Gradual Typing (AGT) [Ronald Garcia et al., 2016], and the Gradualizer [Matteo Cimini and Jeremy Siek, 2016]. In this work, we consider the AGT methodology as it naturally scales to auxiliary structures such as a mutable heap. The AGT methodology helps to systematically construct gradually-typed languages by using abstract interpretation [Cousot and Cousot, 1977] at the type level. In brief, AGT interprets gradual types as an abstraction of sets of possible static types, formally captured through a Galois connection. The static semantics of a gradual language are then derived by lifting the semantics of a statically-typed language through this connection, and the dynamic semantics follow by Curry-Howard from proof normalization of the type safety argument. The AGT methodology has been shown to be effective in many contexts: records and subtyping [Ronald Garcia et al., 2016], type-and-effects [Bañados Schwerter et al., 2014; Bañados Schwerter et al., 2016], refinement types [Nico Lehmann and Éric Tanter, 2017; Niki Vazou et al., 2018], set-theoretic and union types [Castagna and Lanvin, 2017; Matías Toro and Éric Tanter, 2017], information-flow typing [Matías Toro et al., 2018], and parametric polymorphism [Matías Toro et al., 2019]. However, this methodology has never been applied to mutable references in isolation. Although Toro et al. [Matías Toro et al., 2018] apply AGT to a language with references, they only gradualize security levels of types (e.g. Ref Int_?), not whole types (e.g. Ref ? is not supported). In this article we answer the following open questions: Which semantics for gradually-type references follows by systematically applying AGT? Does AGT justify one of the existing approaches, or does it suggest yet another design? Can we recover other semantics for gradual references, if yes, how? This article first reviews the different existing gradual approaches to mutable references through examples. It then presents the semantics for gradual references that is obtained by applying AGT, and how to accommodate the other semantics. More specifically, this work makes the following contributions: - We present λ_REF~, a gradual language with support for mutable references. We derive λ_REF~ by applying the AGT methodology to a fully-static simple language with mutable references called λ_REF. This is the first application of AGT that focuses on gradually-typed mutable references. - We prove that λ_REF~ satisfies the gradual guarantee of Siek et al. [Siek et al., 2015]. We also present the first formal statement and proof of the conservative extension of the dynamic semantics of the static language [Siek et al., 2015], for a gradual language derived using AGT. - We prove that the derived language, λ_REF~, corresponds to the semantics of guarded references from HCC. Formally, given a λ_REF~ term and its compilation to HCC^+ (an adapted version of HCC extended with conditionals and binary operations) we prove that both terms are bisimilar, and that consequently they either both terminate, both fail, or both diverge. - We observe that λ_REF~ and HCC^+ differ in the order of combination of runtime checks. As a result, HCC is space efficient whereas λ_REF~ is not: we can write programs in λ_REF~ that may accumulate an unbounded number of checks. We formalize the changes needed in the dynamic semantics of λ_REF~ to achieve space efficiency. This technique to recover space efficiency is in fact independent from mutable references, and is therefore applicable to other gradual languages derived with AGT. - We formally describe how to support other gradual reference semantics in λ_REF~ by presenting λ_REF~^𝗉𝗆, an extension that additionally supports both permissive and monotonic references. Finally, we prove for the first time that monotonic references satisfy the dynamic gradual guarantee, a non-trivial result that requires careful consideration of updates to the store. Additionally, we implemented λ_REF~ as an interactive prototype that displays both typing derivations and reduction traces. All the examples mentioned in this paper are readily available in the online prototype available at https://pleiad.cl/grefs. As a result, this paper sheds further light on the design space of gradual languages with mutable references and contributes to deepening the understanding of the AGT methodology.

Cite as

Matías Toro and Éric Tanter. Abstracting Gradual References (SCICO Journal-first). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 33:1-33:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{toro_et_al:LIPIcs.ECOOP.2020.33,
  author =	{Toro, Mat{\'\i}as and Tanter, \'{E}ric},
  title =	{{Abstracting Gradual References}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{33:1--33:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.33},
  URN =		{urn:nbn:de:0030-drops-131900},
  doi =		{10.4230/LIPIcs.ECOOP.2020.33},
  annote =	{Keywords: Gradual Typing, Mutable References, Abstract interpretation}
}

Document

DOI: 10.4230/DagRep.8.5.1

Secure Compilation (Dagstuhl Seminar 18201)

Authors: Amal Ahmed, Deepak Garg, Catalin Hritcu, and Frank Piessens

Published in: Dagstuhl Reports, Volume 8, Issue 5 (2019)

Abstract

Secure compilation is an emerging field that puts together advances in security, programming languages, verification, systems, and hardware architectures in order to devise secure compilation chains that eliminate many of today's vulnerabilities. Secure compilation aims to protect a source language's abstractions in compiled code, even against low-level attacks. For a concrete example, all modern languages provide a notion of structured control flow and an invoked procedure is expected to return to the right place. However, today's compilation chains (compilers, linkers, loaders, runtime systems, hardware) cannot efficiently enforce this abstraction: linked low-level code can call and return to arbitrary instructions or smash the stack, blatantly violating the high-level abstraction. The emerging secure compilation community aims to address such problems by devising formal security criteria, efficient enforcement mechanisms, and effective proof techniques. This seminar strived to take a broad and inclusive view of secure compilation and to provide a forum for discussion on the topic. The goal was to identify interesting research directions and open challenges by bringing together people working on building secure compilation chains, on developing proof techniques and verification tools, and on designing security mechanisms.

Cite as

Amal Ahmed, Deepak Garg, Catalin Hritcu, and Frank Piessens. Secure Compilation (Dagstuhl Seminar 18201). In Dagstuhl Reports, Volume 8, Issue 5, pp. 1-30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{ahmed_et_al:DagRep.8.5.1,
  author =	{Ahmed, Amal and Garg, Deepak and Hritcu, Catalin and Piessens, Frank},
  title =	{{Secure Compilation (Dagstuhl Seminar 18201)}},
  pages =	{1--30},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{5},
  editor =	{Ahmed, Amal and Garg, Deepak and Hritcu, Catalin and Piessens, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.5.1},
  URN =		{urn:nbn:de:0030-drops-98911},
  doi =		{10.4230/DagRep.8.5.1},
  annote =	{Keywords: secure compilation, low-level attacks, source-level reasoning, attacker models, full abstraction, hyperproperties, enforcement mechanisms, compartmentalization, security architectures, side-channels}
}

Document

DOI: 10.4230/LIPIcs.SNAPL.2017.12

Linking Types for Multi-Language Software: Have Your Cake and Eat It Too

Authors: Daniel Patterson and Amal Ahmed

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract

Large software systems are and should be implemented with many different languages, each suited to the domain of the task at hand. High-level business logic may be written in Java or OCaml, resource-intensive components may be written in C or Rust, and high-assurance components may be written in Coq. In some development shops, domain-specific languages are used in various parts of systems to better separate the logic of particular problems from the plumbing of general-purpose programming. But how are programmers to reason about such multi-language systems? Currently, for a programmer to reason about a single source component within this multi-language system, it is not sufficient for her to consider how her component behaves in source-level contexts. Instead, she is required to understand the target contexts that her component will be run in after compilation - which requires not only understanding aspects of the compiler, but also how target components are linked together. These target contexts may have behavior inexpressible in the source, which can impact the notion of equivalence that justifies behavior-preserving modifications of code, whether programmer refactorings or compiler optimizations. But while programmers should not have to reason about arbitrary target contexts, sometimes multi-language linking is done exactly to gain access to features unavailable in the source. To enable programmers to reason about components that link with behavior inexpressible in their language, we advocate that language designers incorporate specifications for linking into the source language. Such specifications should allow a programmer to reason about inputs from other languages in a way that remains close to the semantics of her language. Linking types are a well-specified minimal extension of a source language that allow programmers to annotate where in their programs they can link with components that are not expressible in their unadulterated source language. This gives them fine-grained control over the contexts that they must reason about and the equivalences that arise.

Cite as

Daniel Patterson and Amal Ahmed. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 12:1-12:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{patterson_et_al:LIPIcs.SNAPL.2017.12,
  author =	{Patterson, Daniel and Ahmed, Amal},
  title =	{{Linking Types for Multi-Language Software: Have Your Cake and Eat It Too}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.12},
  URN =		{urn:nbn:de:0030-drops-71250},
  doi =		{10.4230/LIPIcs.SNAPL.2017.12},
  annote =	{Keywords: Linking, program reasoning, equivalence, expressive power of languages, fully abstract compilation}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2016.1

Compositional Compiler Verification for a Multi-Language World

Authors: Amal Ahmed

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

Abstract

Verified compilers are typically proved correct under severe restrictions on what the compiler's output may be linked with, from no linking at all to linking only with code compiled from the same source language. Such assumptions contradict the reality of how we use these compilers since most software systems today are comprised of components written in different languages compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language. The key challenge in verifying compilers for today's world of multi-language software is how to formally state a compiler correctness theorem that is compositional along two dimensions. First, the theorem must guarantee correct compilation of components while allowing compiled code to be composed (linked) with target-language components of arbitrary provenance, including those compiled from other languages. Second, the theorem must support verification of multi-pass compilers by composing correctness proofs for individual passes. In this talk, I will describe a methodology for verifying compositional compiler correctness for a higher-order typed language and discuss the challenges that lie ahead. I will argue that compositional compiler correctness is, in essence, a language interoperability problem: for viable solutions in the long term, high-level languages must be equipped with principled foreign-function interfaces that specify safe interoperability between high-level and low-level components, and between more precisely and less precisely typed code.

Cite as

Amal Ahmed. Compositional Compiler Verification for a Multi-Language World. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{ahmed:LIPIcs.FSCD.2016.1,
  author =	{Ahmed, Amal},
  title =	{{Compositional Compiler Verification for a Multi-Language World}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{1:1--1:1},
  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.1},
  URN =		{urn:nbn:de:0030-drops-59680},
  doi =		{10.4230/LIPIcs.FSCD.2016.1},
  annote =	{Keywords: verified compilation; compositional compiler correctness, multi-language semantics, typed low-level languages}
}

Document

DOI: 10.4230/LIPIcs.SNAPL.2015.15

Verified Compilers for a Multi-Language World

Authors: Amal Ahmed

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

Abstract

Though there has been remarkable progress on formally verified compilers in recent years, most of these compilers suffer from a serious limitation: they are proved correct under the assumption that they will only be used to compile whole programs. This is an unrealistic assumption since most software systems today are comprised of components written in different languages - both typed and untyped - compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language. We are pursuing a new methodology for building verified compilers for today's world of multi-language software. The project has two central themes, both of which stem from a view of compiler correctness as a language interoperability problem. First, to specify correctness of component compilation, we require that if a source component s compiles to target component t, then t linked with some arbitrary target code t' should behave the same as s interoperating with t'. The latter demands a formal semantics of interoperability between the source and target languages. Second, to enable safe interoperability between components compiled from languages as different as ML, Rust, Python, and C, we plan to design a gradually type-safe target language based on LLVM that supports safe interoperability between more precisely typed, less precisely typed, and type-unsafe components. Our approach opens up a new avenue for exploring sensible language interoperability while also tackling compiler correctness.

Cite as

Amal Ahmed. Verified Compilers for a Multi-Language World. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 15-31, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ahmed:LIPIcs.SNAPL.2015.15,
  author =	{Ahmed, Amal},
  title =	{{Verified Compilers for a Multi-Language World}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{15--31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodí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.15},
  URN =		{urn:nbn:de:0030-drops-50131},
  doi =		{10.4230/LIPIcs.SNAPL.2015.15},
  annote =	{Keywords: verified compilation, compositional compiler correctness, multi-language semantics, typed low-level languages, gradual typing}
}

Document

DOI: 10.4230/DagSemProc.10351.1

10351 Abstracts Collection – Modelling, Controlling and Reasoning About State

Authors: Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351 ``Modelling, Controlling and Reasoning About State '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. Links to extended abstracts or full papers are provided, if available.

Cite as

Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Abstracts Collection – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:DagSemProc.10351.1,
  author =	{Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin},
  title =	{{10351 Abstracts Collection – Modelling, Controlling and Reasoning About State}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.1},
  URN =		{urn:nbn:de:0030-drops-28116},
  doi =		{10.4230/DagSemProc.10351.1},
  annote =	{Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification}
}

Document

DOI: 10.4230/DagSemProc.10351.2

10351 Executive Summary – Modelling, Controlling and Reasoning About State

Authors: Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

From 29 August 2010 to 3 September 2010, the Dagstuhl Seminar 10351 ``Modelling, Controlling and Reasoning About State '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. 44 researchers, with interests and expertise in many different aspects of modelling and reasoning about mutable state, met to present their current work and discuss ongoing projects and open problems. This executive summary provides a general overview of the goals of the seminar and of the topics discussed.

Cite as

Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann. 10351 Executive Summary – Modelling, Controlling and Reasoning About State. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:DagSemProc.10351.2,
  author =	{Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin},
  title =	{{10351 Executive Summary – Modelling, Controlling and Reasoning About State}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.2},
  URN =		{urn:nbn:de:0030-drops-28108},
  doi =		{10.4230/DagSemProc.10351.2},
  annote =	{Keywords: Mutable State, Program Logics, Semantics, Type Systems, Verification}
}

Document

DOI: 10.4230/DagSemProc.10351.3

A Theory of Termination via Indirection

Authors: Robert Dockins and Aquinas Hobor

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

Step-indexed models provide approximations to a class of domain equations and can prove type safety, partial correctness, and program equivalence; however, a common misconception is that they are inapplicable to liveness problems. We disprove this by applying step-indexing to develop the first Hoare logic of total correctness for a language with function pointers and semantic assertions. In fact, from a liveness perspective, our logic is stronger: we verify explicit time resource bounds. We apply our logic to examples containing nontrivial "higher-order" uses of function pointers and we prove soundness with respect to a standard operational semantics. Our core technique is very compact and may be applicable to other liveness problems. Our results are machine checked in Coq.

Cite as

Robert Dockins and Aquinas Hobor. A Theory of Termination via Indirection. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dockins_et_al:DagSemProc.10351.3,
  author =	{Dockins, Robert and Hobor, Aquinas},
  title =	{{A Theory of Termination via Indirection}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.3},
  URN =		{urn:nbn:de:0030-drops-28050},
  doi =		{10.4230/DagSemProc.10351.3},
  annote =	{Keywords: Step-indexed Models, Termination}
}

Document

DOI: 10.4230/DagSemProc.10351.4

Limitations of Applicative Bisimulation (Preliminary Report)

Authors: Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

We present a series of examples that illuminate an important aspect of the semantics of higher-order functions with local state. Namely that certain behaviour of such functions can only be observed by pro- viding them with arguments that contain the functions themselves. This provides evidence for the necessity of complex conditions for functions in modern semantics for state, such as logical relations and Kripke-like bisimulations, where related functions are applied to related arguments (that may contain the functions). It also suggests that simpler semantics, such as those based on applicative bisimulations where functions are ap- plied to identical arguments, would not scale to higher-order languages with local state.

Cite as

Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{koutavas_et_al:DagSemProc.10351.4,
  author =	{Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro},
  title =	{{Limitations of Applicative Bisimulation (Preliminary Report)}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.4},
  URN =		{urn:nbn:de:0030-drops-28074},
  doi =		{10.4230/DagSemProc.10351.4},
  annote =	{Keywords: Imperative languages, higher-order functions, local state}
}

Document

DOI: 10.4230/DagSemProc.10351.5

Program Equivalence with Names

Authors: Nikos Tzevelekos

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

The nu-calculus of Pitts and Stark was introduced as a paradigmatic functional language with a very basic local-state effect: references of unit type. These were called names, and the motto of the new language went as follows: "Names are created with local scope, can be tested for equality, and are passed around via function application, but that is all." Because of this limited framework, the hope was that fully abstract models and complete proof techniques could be obtained. However, it was soon realised that the behaviour of nu-calculus programs is quite intricate, and program equivalence in particular is surprisingly difficult to capture. Here we shall focus on the following "hard" equivalence. new x,y in f. (fx=fy) == f. true We shall examine attempts and proofs of the above, explain the advantages and disadvantages of the proof methods and discuss why program equivalence in this simple language remains to date a mystery.

Cite as

Nikos Tzevelekos. Program Equivalence with Names. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{tzevelekos:DagSemProc.10351.5,
  author =	{Tzevelekos, Nikos},
  title =	{{Program Equivalence with Names}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.5},
  URN =		{urn:nbn:de:0030-drops-28092},
  doi =		{10.4230/DagSemProc.10351.5},
  annote =	{Keywords: Nu-calculus, Local State, Logical Relations, Game Semantics, Environmental Bisimulations}
}

Document

DOI: 10.4230/DagSemProc.10351.6

Step-Indexed Biorthogonality: a Tutorial Example

Authors: Andrew M. Pitts

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

The purpose of this note is to illustrate the use of step-indexing combined with biorthogonality to construct syntactical logical relations. It walks through the details of a syntactically simple, yet non-trivial example: a proof of the "CIU Theorem'' for contextual equivalence in the untyped call-by-value $lambda$-calculus with recursively defined functions.

Cite as

Andrew M. Pitts. Step-Indexed Biorthogonality: a Tutorial Example. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{pitts:DagSemProc.10351.6,
  author =	{Pitts, Andrew M.},
  title =	{{Step-Indexed Biorthogonality: a Tutorial Example}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.6},
  URN =		{urn:nbn:de:0030-drops-28067},
  doi =		{10.4230/DagSemProc.10351.6},
  annote =	{Keywords: Biorthogonality, logical relations, operational semantics, step-indexing}
}

Document

DOI: 10.4230/DagSemProc.10351.7

Step-Indexing: The Good, the Bad and the Ugly

Authors: Nick Benton and Chung-Kil Hur

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract

Over the last decade, step-indices have been widely used for the construction of operationally-based logical relations in the presence of various kinds of recursion. We first give an argument that step-indices, or something like them, seem to be required for defining realizability relations between high-level source languages and low-level targets, in the case that the low-level allows egregiously intensional operations such as reflection or comparison of code pointers. We then show how, much to our annoyance, step-indices also seem to prevent us from exploiting such operations as aggressively as we would like in proving program transformations.

Cite as

Nick Benton and Chung-Kil Hur. Step-Indexing: The Good, the Bad and the Ugly. In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{benton_et_al:DagSemProc.10351.7,
  author =	{Benton, Nick and Hur, Chung-Kil},
  title =	{{Step-Indexing: The Good, the Bad and the Ugly}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.7},
  URN =		{urn:nbn:de:0030-drops-28085},
  doi =		{10.4230/DagSemProc.10351.7},
  annote =	{Keywords: Step-Indexing, Logical Relations, Low-Level Languages, Compiler Correctness}
}

Document

DOI: 10.4230/DagSemProc.08061.1

08061 Abstracts Collection – Types, Logics and Semantics for State

Authors: Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)

Abstract

From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 ``Types, Logics and Semantics for State'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett. 08061 Abstracts Collection – Types, Logics and Semantics for State. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:DagSemProc.08061.1,
  author =	{Ahmed, Amal and Benton, Nick and Hofmann, Martin and Morrisett, Greg},
  title =	{{08061 Abstracts Collection – Types, Logics and Semantics for State}},
  booktitle =	{Types, Logics and Semantics for State},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8061},
  editor =	{Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.1},
  URN =		{urn:nbn:de:0030-drops-14281},
  doi =		{10.4230/DagSemProc.08061.1},
  annote =	{Keywords: Mutable State, Program Logics, Semantics, Type Systems, Program Analysis}
}

Document

DOI: 10.4230/DagSemProc.08061.2

08061 Executive Summary – Types, Logics and Semantics for State

Authors: Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett

Published in: Dagstuhl Seminar Proceedings, Volume 8061, Types, Logics and Semantics for State (2008)

Abstract

From 3 February to 8 February 2008, the Dagstuhl Seminar 08061 State" Conference and Research Center (IBFI), Schloss Dagstuhl. 45 researchers, with interests and expertise in many different aspects of modelling and reasoning about mutable state, met to present their current work and discuss ongoing projects and open problems.

Cite as

Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett. 08061 Executive Summary – Types, Logics and Semantics for State. In Types, Logics and Semantics for State. Dagstuhl Seminar Proceedings, Volume 8061, pp. 1-3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{ahmed_et_al:DagSemProc.08061.2,
  author =	{Ahmed, Amal and Benton, Nick and Hofmann, Martin and Morrisett, Greg},
  title =	{{08061 Executive Summary – Types, Logics and Semantics for State}},
  booktitle =	{Types, Logics and Semantics for State},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8061},
  editor =	{Amal Ahmed and Nick Benton and Martin Hofmann and Greg Morrisett},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08061.2},
  URN =		{urn:nbn:de:0030-drops-14269},
  doi =		{10.4230/DagSemProc.08061.2},
  annote =	{Keywords: Mutable State, Program Logics, Semantics, Type Systems, Program Analysis}
}

16 Search Results for "Ahmed, Amal"

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

Abstract

Cite as

Thanks for your feedback!

Could not send message