Search Results

Documents authored by Ahmed, Amal

Document
DOI: 10.4230/DagRep.11.6.54
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
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 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.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.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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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