26 Search Results for "Morriset, Greg"

Volume

LIPIcs, Volume 32

1st Summit on Advances in Programming Languages (SNAPL 2015)

SNAPL 2015, May 3-6, 2015, Asilomar, California, US

Editors: Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morriset

Document
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2015
LIPIcs, Volume 32, SNAPL'15, Complete Volume

Authors: Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett

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

Abstract
LIPIcs, Volume 32, SNAPL'15, Complete Volume
Cite as

Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett. LIPIcs, Volume 32, SNAPL'15, Complete Volume. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{ball_et_al:LIPIcs.SNAPL.2015,
  title =	{{LIPIcs, Volume 32, SNAPL'15, Complete Volume}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  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},
  URN =		{urn:nbn:de:0030-drops-50461},
  doi =		{10.4230/LIPIcs.SNAPL.2015},
  annote =	{Keywords: Programming Languages}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.SNAPL.2015.i
Title, Table of Contents, Preface, List of Authors

Authors: Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morriset

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

Abstract
Title, Table of Contents, Preface, List of Authors
Cite as

Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morriset. Title, Table of Contents, Preface, List of Authors. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. i-xiv, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:LIPIcs.SNAPL.2015.i,
  author =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  title =	{{Title, Table of Contents, Preface, List of Authors}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{i--xiv},
  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.i},
  URN =		{urn:nbn:de:0030-drops-50119},
  doi =		{10.4230/LIPIcs.SNAPL.2015.i},
  annote =	{Keywords: Title, Table of Contents, Preface, List of Authors}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.1
Coupling Memory and Computation for Locality Management

Authors: Umut A. Acar, Guy Blelloch, Matthew Fluet, Stefan K. Muller, and Ram Raghunathan

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

Abstract
We articulate the need for managing (data) locality automatically rather than leaving it to the programmer, especially in parallel programming systems. To this end, we propose techniques for coupling tightly the computation (including the thread scheduler) and the memory manager so that data and computation can be positioned closely in hardware. Such tight coupling of computation and memory management is in sharp contrast with the prevailing practice of considering each in isolation. For example, memory-management techniques usually abstract the computation as an unknown "mutator", which is treated as a "black box". As an example of the approach, in this paper we consider a specific class of parallel computations, nested-parallel computations. Such computations dynamically create a nesting of parallel tasks. We propose a method for organizing memory as a tree of heaps reflecting the structure of the nesting. More specifically, our approach creates a heap for a task if it is separately scheduled on a processor. This allows us to couple garbage collection with the structure of the computation and the way in which it is dynamically scheduled on the processors. This coupling enables taking advantage of locality in the program by mapping it to the locality of the hardware. For example for improved locality a heap can be garbage collected immediately after its task finishes when the heap contents is likely in cache.
Cite as

Umut A. Acar, Guy Blelloch, Matthew Fluet, Stefan K. Muller, and Ram Raghunathan. Coupling Memory and Computation for Locality Management. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 1-14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{acar_et_al:LIPIcs.SNAPL.2015.1,
  author =	{Acar, Umut A. and Blelloch, Guy and Fluet, Matthew and Muller, Stefan K. and Raghunathan, Ram},
  title =	{{Coupling Memory and Computation for Locality Management}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{1--14},
  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.1},
  URN =		{urn:nbn:de:0030-drops-50121},
  doi =		{10.4230/LIPIcs.SNAPL.2015.1},
  annote =	{Keywords: Parallel computing, locality, memory management, parallel garbage collection, functional programming, nested parallelism, thread scheduling}
}
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/LIPIcs.SNAPL.2015.32
Growing a Software Language for Hardware Design

Authors: Joshua Auerbach, David F. Bacon, Perry Cheng, Stephen J. Fink, Rodric Rabbah, and Sunil Shukla

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

Abstract
The Liquid Metal project at IBM Research aimed to design and implement a new programming language called Lime to address some of the challenges posed by heterogeneous systems. Lime is a Java-compatible programming language with features designed to facilitate high level synthesis to hardware (FPGAs). This article reviews the language design from the outset, and highlights some of the earliest design decisions. We also describe how these decisions were revised recently to accommodate important requirements that arise in networking and cryptography.
Cite as

Joshua Auerbach, David F. Bacon, Perry Cheng, Stephen J. Fink, Rodric Rabbah, and Sunil Shukla. Growing a Software Language for Hardware Design. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 32-40, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{auerbach_et_al:LIPIcs.SNAPL.2015.32,
  author =	{Auerbach, Joshua and Bacon, David F. and Cheng, Perry and Fink, Stephen J. and Rabbah, Rodric and Shukla, Sunil},
  title =	{{Growing a Software Language for Hardware Design}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{32--40},
  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.32},
  URN =		{urn:nbn:de:0030-drops-50144},
  doi =		{10.4230/LIPIcs.SNAPL.2015.32},
  annote =	{Keywords: Heterogeneous Systems, FPGA, High Level Synthesis, Dataflow, Functional Programming, Streaming, Java}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.41
Programming with "Big Code": Lessons, Techniques and Applications

Authors: Pavol Bielik, Veselin Raychev, and Martin Vechev

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

Abstract
Programming tools based on probabilistic models of massive codebases (aka "Big Code") promise to solve important programming tasks that were difficult or practically infeasible to address before. However, building such tools requires solving a number of hard problems at the intersection of programming languages, program analysis and machine learning. In this paper we summarize some of our experiences and insights obtained by developing several such probabilistic systems over the last few years (some of these systems are regularly used by thousands of developers worldwide). We hope these observations can provide a guideline for others attempting to create such systems. We also present a prediction approach we find suitable as a starting point for building probabilistic tools, and discuss a practical framework implementing this approach, called Nice2Predict. We release the Nice2Predict framework publicly - the framework can be immediately used as a basis for developing new probabilistic tools. Finally, we present programming applications that we believe will benefit from probabilistic models and should be investigated further.
Cite as

Pavol Bielik, Veselin Raychev, and Martin Vechev. Programming with "Big Code": Lessons, Techniques and Applications. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 41-50, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bielik_et_al:LIPIcs.SNAPL.2015.41,
  author =	{Bielik, Pavol and Raychev, Veselin and Vechev, Martin},
  title =	{{Programming with "Big Code": Lessons, Techniques and Applications}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{41--50},
  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.41},
  URN =		{urn:nbn:de:0030-drops-50152},
  doi =		{10.4230/LIPIcs.SNAPL.2015.41},
  annote =	{Keywords: probabilistic tools, probabilistic inference and learning, program analysis, open-source software}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.51
Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis

Authors: Alvin Cheung, Shoaib Kamil, and Armando Solar-Lezama

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

Abstract
This paper describes a new approach to program optimization that allows general purpose code to benefit from the optimization power of domain-specific compilers. The key to this approach is a synthesis-based technique to raise the level of abstraction of general-purpose code to enable aggressive domain-specific optimizations. We have been implementing this approach in an extensible system called Herd. The system is designed around a collection of parameterized kernel translators. Each kernel translator is associated with a domain-specific compiler, and the role of each kernel translator is to scan the input code in search of code fragments that can be optimized by the domain-specific compiler embedded within each kernel translator. By leveraging general synthesis technology, it is possible to have a generic kernel translator that can be specialized by compiler developers for each domain-specific compiler, making it easy to build new domain knowledge into the overall system. We illustrate this new approach to build optimizing compilers in two different domains, and highlight research challenges that need to be addressed in order to achieve the ultimate vision.
Cite as

Alvin Cheung, Shoaib Kamil, and Armando Solar-Lezama. Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 51-62, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cheung_et_al:LIPIcs.SNAPL.2015.51,
  author =	{Cheung, Alvin and Kamil, Shoaib and Solar-Lezama, Armando},
  title =	{{Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{51--62},
  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.51},
  URN =		{urn:nbn:de:0030-drops-50162},
  doi =		{10.4230/LIPIcs.SNAPL.2015.51},
  annote =	{Keywords: compilers, domain-specific languages, program synthesis, cross compilation, verification}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.63
Yedalog: Exploring Knowledge at Scale

Authors: Brian Chin, Daniel von Dincklage, Vuk Ercegovac, Peter Hawkins, Mark S. Miller, Franz Och, Christopher Olston, and Fernando Pereira

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

Abstract
With huge progress on data processing frameworks, human programmers are frequently the bottleneck when analyzing large repositories of data. We introduce Yedalog, a declarative programming language that allows programmers to mix data-parallel pipelines and computation seamlessly in a single language. By contrast, most existing tools for data-parallel computation embed a sublanguage of data-parallel pipelines in a general-purpose language, or vice versa. Yedalog extends Datalog, incorporating not only computational features from logic programming, but also features for working with data structured as nested records. Yedalog programs can run both on a single machine, and distributed across a cluster in batch and interactive modes, allowing programmers to mix different modes of execution easily.
Cite as

Brian Chin, Daniel von Dincklage, Vuk Ercegovac, Peter Hawkins, Mark S. Miller, Franz Och, Christopher Olston, and Fernando Pereira. Yedalog: Exploring Knowledge at Scale. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 63-78, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chin_et_al:LIPIcs.SNAPL.2015.63,
  author =	{Chin, Brian and von Dincklage, Daniel and Ercegovac, Vuk and Hawkins, Peter and Miller, Mark S. and Och, Franz and Olston, Christopher and Pereira, Fernando},
  title =	{{Yedalog: Exploring Knowledge at Scale}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{63--78},
  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.63},
  URN =		{urn:nbn:de:0030-drops-50172},
  doi =		{10.4230/LIPIcs.SNAPL.2015.63},
  annote =	{Keywords: Datalog, MapReduce}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.79
The Design of Terra: Harnessing the Best Features of High-Level and Low-Level Languages

Authors: Zachary DeVito and Pat Hanrahan

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

Abstract
Applications are often written using a combination of high-level and low-level languages since it allows performance critical parts to be carefully optimized, while other parts can be written more productively. This approach is used in web development, game programming, and in build systems for applications themselves. However, most languages were not designed with interoperability in mind, resulting in glue code and duplicated features that add complexity. We propose a two-language system where both languages were designed to interoperate. Lua is used for our high-level language since it was originally designed with interoperability in mind. We create a new low-level language, Terra, that we designed to interoperate with Lua. It is embedded in Lua, and meta-programmed from it, but has a low level of abstraction suited for writing high-performance code. We discuss important design decisions - compartmentalized runtimes, glue-free interoperation, and meta-programming features - that enable Lua and Terra to be more powerful than the sum of their parts.
Cite as

Zachary DeVito and Pat Hanrahan. The Design of Terra: Harnessing the Best Features of High-Level and Low-Level Languages. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 79-89, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{devito_et_al:LIPIcs.SNAPL.2015.79,
  author =	{DeVito, Zachary and Hanrahan, Pat},
  title =	{{The Design of Terra: Harnessing the Best Features of High-Level and Low-Level Languages}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{79--89},
  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.79},
  URN =		{urn:nbn:de:0030-drops-50186},
  doi =		{10.4230/LIPIcs.SNAPL.2015.79},
  annote =	{Keywords: language interoperability, meta-programming, high-performance, Lua}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.90
The Need for Language Support for Fault-Tolerant Distributed Systems

Authors: Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey

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

Abstract
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. Nonetheless there is surprisingly little language and verification support to build distributed systems based on fault-tolerant algorithms. In this paper, we present some of the challenges that a designer has to overcome to implement a fault-tolerant distributed system. Then we review different models that have been proposed to reason about distributed algorithms and sketch how such a model can form the basis for a domain-specific programming language. Adopting a high-level programming model can simplify the programmer's life and make the code amenable to automated verification, while still compiling to efficiently executable code. We conclude by summarizing the current status of an ongoing language design and implementation project that is based on this idea.
Cite as

Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. The Need for Language Support for Fault-Tolerant Distributed Systems. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 90-102, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dragoi_et_al:LIPIcs.SNAPL.2015.90,
  author =	{Dragoi, Cezara and Henzinger, Thomas A. and Zufferey, Damien},
  title =	{{The Need for Language Support for Fault-Tolerant Distributed Systems}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{90--102},
  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.90},
  URN =		{urn:nbn:de:0030-drops-50192},
  doi =		{10.4230/LIPIcs.SNAPL.2015.90},
  annote =	{Keywords: Programming language, Fault-tolerant distributed algorithms, Automated verification}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.103
Toward a Dependability Case Language and Workflow for a Radiation Therapy System

Authors: Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang

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

Abstract
We present a near-future research agenda for bringing a suite of modern programming-languages verification tools - specifically interactive theorem proving, solver-aided languages, and formally defined domain-specific languages - to the development of a specific safety-critical system, a radiotherapy medical device. We sketch how we believe recent programming-languages research advances can merge with existing best practices for safety-critical systems to increase system assurance and developer productivity. We motivate hypotheses central to our agenda: That we should start with a single specific system and that we need to integrate a variety of complementary verification and synthesis tools into system development.
Cite as

Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. Toward a Dependability Case Language and Workflow for a Radiation Therapy System. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 103-112, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{ernst_et_al:LIPIcs.SNAPL.2015.103,
  author =	{Ernst, Michael D. and Grossman, Dan and Jacky, Jon and Loncaric, Calvin and Pernsteiner, Stuart and Tatlock, Zachary and Torlak, Emina and Wang, Xi},
  title =	{{Toward a Dependability Case Language and Workflow for a Radiation Therapy System}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{103--112},
  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.103},
  URN =		{urn:nbn:de:0030-drops-50208},
  doi =		{10.4230/LIPIcs.SNAPL.2015.103},
  annote =	{Keywords: Synthesis, Proof Assistants, Verification, Dependability Cases, Domain Specific Languages, Radiation Therapy}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.113
The Racket Manifesto

Authors: Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt

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

Abstract
The creation of a programming language calls for guiding principles that point the developers to goals. This article spells out the three basic principles behind the 20-year development of Racket. First, programming is about stating and solving problems, and this activity normally takes place in a context with its own language of discourse; good programmers ought to formulate this language as a programming language. Hence, Racket is a programming language for creating new programming languages. Second, by following this language-oriented approach to programming, systems become multi-lingual collections of interconnected components. Each language and component must be able to protect its specific invariants. In support, Racket offers protection mechanisms to implement a full language spectrum, from C-level bit manipulation to soundly typed extensions. Third, because Racket considers programming as problem solving in the correct language, Racket also turns extra-linguistic mechanisms into linguistic constructs, especially mechanisms for managing resources and projects. The paper explains these principles and how Racket lives up to them, presents the evaluation framework behind the design process, and concludes with a sketch of Racket's imperfections and opportunities for future improvements.
Cite as

Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. The Racket Manifesto. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 113-128, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{felleisen_et_al:LIPIcs.SNAPL.2015.113,
  author =	{Felleisen, Matthias and Findler, Robert Bruce and Flatt, Matthew and Krishnamurthi, Shriram and Barzilay, Eli and McCarthy, Jay and Tobin-Hochstadt, Sam},
  title =	{{The Racket Manifesto}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{113--128},
  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.113},
  URN =		{urn:nbn:de:0030-drops-50211},
  doi =		{10.4230/LIPIcs.SNAPL.2015.113},
  annote =	{Keywords: design guidelines, language generation, full-spectrum language}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.129
A Theory AB Toolbox

Authors: Marco Gaboardi and Justin Hsu

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

Abstract
Randomized algorithms are a staple of the theoretical computer science literature. By careful use of randomness, algorithms can achieve properties that are simply not possible with deterministic algorithms. Today, these properties are proved on paper, by theoretical computer scientists; we investigate formally verifying these proofs. The main challenges are two: proofs about algorithms can be quite complex, using various facts from probability theory; and proofs are highly customized - two proofs of the same property for two algorithms can be completely different. To overcome these challenges, we propose taking inspiration from paper proofs, by building common tools - abstractions, reasoning principles, perhaps even notations - into a formal verification toolbox. To give an idea of our approach, we consider three common patterns in paper proofs: the union bound, concentration bounds, and martingale arguments.
Cite as

Marco Gaboardi and Justin Hsu. A Theory AB Toolbox. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 129-139, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gaboardi_et_al:LIPIcs.SNAPL.2015.129,
  author =	{Gaboardi, Marco and Hsu, Justin},
  title =	{{A Theory AB Toolbox}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{129--139},
  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.129},
  URN =		{urn:nbn:de:0030-drops-50225},
  doi =		{10.4230/LIPIcs.SNAPL.2015.129},
  annote =	{Keywords: Verification, randomized algorithms}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.140
Tracking the Flow of Ideas through the Programming Languages Literature

Authors: Michael Greenberg, Kathleen Fisher, and David Walker

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

Abstract
How have conferences like ICFP, OOPSLA, PLDI, and POPL evolved over the last 20 years? Did generalizing the Call for Papers for OOPSLA in 2007 or changing the name of the umbrella conference to SPLASH in 2010 have any effect on the kinds of papers published there? How do POPL and PLDI papers compare, topic-wise? Is there related work that I am missing? Have the ideas in O'Hearn's classic paper on separation logic shifted the kinds of papers that appear in POPL? Does a proposed program committee cover the range of submissions expected for the conference? If we had better tools for analyzing the programming language literature, we might be able to answer these questions and others like them in a data-driven way. In this paper, we explore how topic modeling, a branch of machine learning, might help the programming language community better understand our literature.
Cite as

Michael Greenberg, Kathleen Fisher, and David Walker. Tracking the Flow of Ideas through the Programming Languages Literature. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 140-155, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{greenberg_et_al:LIPIcs.SNAPL.2015.140,
  author =	{Greenberg, Michael and Fisher, Kathleen and Walker, David},
  title =	{{Tracking the Flow of Ideas through the Programming Languages Literature}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{140--155},
  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.140},
  URN =		{urn:nbn:de:0030-drops-50232},
  doi =		{10.4230/LIPIcs.SNAPL.2015.140},
  annote =	{Keywords: programming languages literature, topic models, irony}
}
  • Refine by Author
  • 3 Krishnamurthi, Shriram
  • 2 Ball, Thomas
  • 2 Lerner, Benjamin S.
  • 1 Acar, Umut A.
  • 1 Ahmed, Amal
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 gradual typing
  • 2 Verification
  • 2 verification
  • 1 Automated verification
  • 1 Buffer overflows
  • Show More...

  • Refine by Type
  • 25 document
  • 1 volume

  • Refine by Publication Year
  • 26 2015

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact