Volume
LIPIcs, Volume 32
1st Summit on Advances in Programming Languages (SNAPL 2015)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Summit on Advances in Programming Languages (SNAPL)
Event
SNAPL 2015, May 3-6, 2015, Asilomar, California, USEditors
Publication Details
- published at: 2015-04-30
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-80-4
- DBLP: db/conf/snapl/snapl2015
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 32, SNAPL'15, Complete Volume
Abstract
LIPIcs, Volume 32, SNAPL'15, Complete Volume
Cite as
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
Title, Table of Contents, Preface, List of Authors
Abstract
Title, Table of Contents, Preface, List of Authors
Cite as
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
Coupling Memory and Computation for Locality Management
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
Verified Compilers for a Multi-Language World
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
Growing a Software Language for Hardware Design
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
Programming with "Big Code": Lessons, Techniques and Applications
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
Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis
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
Yedalog: Exploring Knowledge at Scale
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
The Design of Terra: Harnessing the Best Features of High-Level and Low-Level Languages
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
The Need for Language Support for Fault-Tolerant Distributed Systems
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
Toward a Dependability Case Language and Workflow for a Radiation Therapy System
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
The Racket Manifesto
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
A Theory AB Toolbox
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
Tracking the Flow of Ideas through the Programming Languages Literature
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}
}
Document
InterPoll: Crowd-Sourced Internet Polls
Abstract
Crowd-sourcing is increasingly being used to provide answers to online polls and surveys. However, existing systems, while taking care of the mechanics of attracting crowd workers, poll building, and payment, provide little to help the survey-maker or pollster in obtaining statistically significant results devoid of even the obvious selection biases.
This paper proposes InterPoll, a platform for programming of crowd-sourced polls. Pollsters express polls as embedded LINQ queries and the runtime correctly reasons about uncertainty in those polls, only polling as many people as required to meet statistical guarantees. To optimize the cost of polls, InterPoll performs query optimization, as well as bias correction and power analysis. The goal of InterPoll is to provide a system that can be reliably used for research into marketing, social and political science questions.
This paper highlights some of the existing challenges and how InterPoll is designed to address most of them.
In this paper we summarize some of the work we have already done and give an outline for future work.
Cite as
Benjamin Livshits and Todd Mytkowicz. InterPoll: Crowd-Sourced Internet Polls. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 156-176, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{livshits_et_al:LIPIcs.SNAPL.2015.156,
author = {Livshits, Benjamin and Mytkowicz, Todd},
title = {{InterPoll: Crowd-Sourced Internet Polls}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {156--176},
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.156},
URN = {urn:nbn:de:0030-drops-50242},
doi = {10.4230/LIPIcs.SNAPL.2015.156},
annote = {Keywords: CrowdSourcing, Polling, LINQ}
}
Document
The Silently Shifting Semicolon
Abstract
Memory consistency models for modern concurrent languages have largely been designed from a system-centric point of view that protects, at all costs, optimizations that were originally designed for sequential programs. The result is a situation that, when viewed from a programmer's standpoint, borders on absurd. We illustrate this unfortunate situation with a brief fable and then examine the opportunities to right our path.
Cite as
Daniel Marino, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy, and Abhayendra Singh. The Silently Shifting Semicolon. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 177-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{marino_et_al:LIPIcs.SNAPL.2015.177,
author = {Marino, Daniel and Millstein, Todd and Musuvathi, Madanlal and Narayanasamy, Satish and Singh, Abhayendra},
title = {{The Silently Shifting Semicolon}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {177--189},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-80-4},
ISSN = {1868-8969},
year = {2015},
volume = {32},
editor = {Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.177},
URN = {urn:nbn:de:0030-drops-50259},
doi = {10.4230/LIPIcs.SNAPL.2015.177},
annote = {Keywords: memory consistency models; sequential consistency; safe programming languages; data races}
}
Document
Everything You Want to Know About Pointer-Based Checking
Abstract
Lack of memory safety in C/C++ has resulted in numerous security vulnerabilities and serious bugs in large software systems. This paper highlights the challenges in enforcing memory safety for C/C++ programs and progress made as part of the SoftBoundCETS project. We have been exploring memory safety enforcement at various levels - in hardware, in the compiler, and as a hardware-compiler hybrid - in this project. Our research has identified that maintaining metadata with pointers in a disjoint metadata space and performing bounds and use-after-free checking can provide comprehensive memory safety. We describe the rationale behind the design decisions and its ramifications on various dimensions, our experience with the various variants that we explored in this project, and the lessons learned in the process. We also describe and analyze the forthcoming Intel Memory Protection Extensions (MPX) that provides hardware acceleration for disjoint metadata and pointer checking in mainstream hardware, which is expected to be available later this year.
Cite as
Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Everything You Want to Know About Pointer-Based Checking. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 190-208, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{nagarakatte_et_al:LIPIcs.SNAPL.2015.190,
author = {Nagarakatte, Santosh and Martin, Milo M. K. and Zdancewic, Steve},
title = {{Everything You Want to Know About Pointer-Based Checking}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {190--208},
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.190},
URN = {urn:nbn:de:0030-drops-50268},
doi = {10.4230/LIPIcs.SNAPL.2015.190},
annote = {Keywords: Memory safety, Buffer overflows, Dangling pointers, Pointer-based checking, SoftBoundCETS}
}
Document
New Directions for Network Verification
Abstract
Network verification has recently gained popularity in the programming languages and verification community. Much of the recent work in this area has focused on verifying the behavior of simple networks, whose actions are dictated by static, immutable rules configured ahead of time. However, in reality, modern networks contain a variety of middleboxes, whose behavior is affected both by their configuration and by mutable state updated in response to packets received by them. In this position paper we critically review recent progress on network verification, propose some next steps towards a more complete form of network verification, dispel some myths about networks, provide a more formal description of our approach, and end with a discussion of the formal questions posed to this community by the network verification agenda.
Cite as
Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, and Scott Shenker. New Directions for Network Verification. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 209-220, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{panda_et_al:LIPIcs.SNAPL.2015.209,
author = {Panda, Aurojit and Argyraki, Katerina and Sagiv, Mooly and Schapira, Michael and Shenker, Scott},
title = {{New Directions for Network Verification}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {209--220},
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.209},
URN = {urn:nbn:de:0030-drops-50278},
doi = {10.4230/LIPIcs.SNAPL.2015.209},
annote = {Keywords: Middleboxes, Network Verification, Mutable Dataplane}
}
Document
A Few Lessons from the Mezzo Project
Abstract
With Mezzo, we set out to design a new, better programming language. In this modest document, we recount our adventure: what worked, and what did not; the decisions that appear in hindsight to have been good, and the design mistakes that cost us; the things that we are happy with in the end, and the frustrating aspects we wish we had handled better.
Cite as
Francois Pottier and Jonathan Protzenko. A Few Lessons from the Mezzo Project. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 221-237, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{pottier_et_al:LIPIcs.SNAPL.2015.221,
author = {Pottier, Francois and Protzenko, Jonathan},
title = {{A Few Lessons from the Mezzo Project}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {221--237},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-80-4},
ISSN = {1868-8969},
year = {2015},
volume = {32},
editor = {Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.221},
URN = {urn:nbn:de:0030-drops-50281},
doi = {10.4230/LIPIcs.SNAPL.2015.221},
annote = {Keywords: static type systems, side effects, aliasing, ownership}
}
Document
Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems
Abstract
Most performance critical software is developed using very low-level techniques. We argue that this needs to change, and that generative programming is an effective avenue to enable the use of high-level languages and programming techniques in many such circumstances.
Cite as
Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth, Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov, Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel, and Kunle Olukotun. Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 238-261, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{rompf_et_al:LIPIcs.SNAPL.2015.238,
author = {Rompf, Tiark and Brown, Kevin J. and Lee, HyoukJoong and Sujeeth, Arvind K. and Jonnalagedda, Manohar and Amin, Nada and Ofenbeck, Georg and Stojanov, Alen and Klonatos, Yannis and Dashti, Mohammad and Koch, Christoph and P\"{u}schel, Markus and Olukotun, Kunle},
title = {{Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {238--261},
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.238},
URN = {urn:nbn:de:0030-drops-50295},
doi = {10.4230/LIPIcs.SNAPL.2015.238},
annote = {Keywords: Performance, Generative Programming, Staging, DSLs}
}
Document
Hardware-Software Co-Design: Not Just a Cliché
Abstract
The age of the air-tight hardware abstraction is over. As the computing ecosystem moves beyond the predictable yearly advances of Moore's Law, appeals to familiarity and backwards compatibility will become less convincing: fundamental shifts in abstraction and design will look more enticing. It is time to embrace hardware-software co-design in earnest, to cooperate between programming languages and architecture to upend legacy constraints on computing. We describe our work on approximate computing, a new avenue spanning the system stack from applications and languages to microarchitectures. We reflect on the challenges and successes of approximation research and, with these lessons in mind, distill opportunities for future hardware-software co-design efforts.
Cite as
Adrian Sampson, James Bornholt, and Luis Ceze. Hardware-Software Co-Design: Not Just a Cliché. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 262-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{sampson_et_al:LIPIcs.SNAPL.2015.262,
author = {Sampson, Adrian and Bornholt, James and Ceze, Luis},
title = {{Hardware-Software Co-Design: Not Just a Clich\'{e}}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {262--273},
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.262},
URN = {urn:nbn:de:0030-drops-50301},
doi = {10.4230/LIPIcs.SNAPL.2015.262},
annote = {Keywords: approximation, co-design, architecture, verification}
}
Document
Refined Criteria for Gradual Typing
Abstract
Siek and Taha [2006] coined the term gradual typing to describe a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines. Since 2006, the term gradual typing has become quite popular but its meaning has become diluted to encompass anything related to the integration of static and dynamic typing. This dilution is partly the fault of the original paper, which provided an incomplete formal characterization of what it means to be gradually typed. In this paper we draw a crisp line in the sand that includes a new formal property, named the gradual guarantee, that relates the behavior of programs that differ only with respect to their type annotations. We argue that the gradual guarantee provides important guidance for designers of gradually typed languages. We survey the gradual typing literature, critiquing designs in light of the gradual guarantee. We also report on a mechanized proof that the gradual guarantee holds for the Gradually Typed Lambda Calculus.
Cite as
Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 274-293, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{siek_et_al:LIPIcs.SNAPL.2015.274,
author = {Siek, Jeremy G. and Vitousek, Michael M. and Cimini, Matteo and Boyland, John Tang},
title = {{Refined Criteria for Gradual Typing}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {274--293},
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.274},
URN = {urn:nbn:de:0030-drops-50312},
doi = {10.4230/LIPIcs.SNAPL.2015.274},
annote = {Keywords: gradual typing, type systems, semantics, dynamic languages}
}
Document
None, One, Many - What's the Difference, Anyhow?
Abstract
We observe that compared to natural and modelling languages, the differences in expression required to deal with no, one, or many objects in programming languages are particularly pronounced. We identify some problems inherent in type-based unifications of different numbers, and advocate a solution that builds on the introduction of multiplicity as a new grammatical category of programming languages.
Cite as
Friedrich Steimann. None, One, Many - What's the Difference, Anyhow?. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 294-308, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{steimann:LIPIcs.SNAPL.2015.294,
author = {Steimann, Friedrich},
title = {{None, One, Many - What's the Difference, Anyhow?}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {294--308},
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.294},
URN = {urn:nbn:de:0030-drops-50329},
doi = {10.4230/LIPIcs.SNAPL.2015.294},
annote = {Keywords: objects, collections, relationships, pointers, multiplicity, null}
}
Document
A Complement to Blame
Abstract
Contracts, gradual typing, and hybrid typing all permit less-precisely typed and more-precisely typed code to interact. Blame calculus encompasses these, and guarantees blame safety: blame for type errors always lays with less-precisely typed code. This paper serves as a complement to the literature on blame calculus: it elaborates on motivation, comments on the reception of the work, critiques some work for not properly attending to blame, and looks forward to applications. No knowledge of contracts, gradual typing, hybrid typing, or blame calculus is assumed.
Cite as
Philip Wadler. A Complement to Blame. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 309-320, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{wadler:LIPIcs.SNAPL.2015.309,
author = {Wadler, Philip},
title = {{A Complement to Blame}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {309--320},
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.309},
URN = {urn:nbn:de:0030-drops-50333},
doi = {10.4230/LIPIcs.SNAPL.2015.309},
annote = {Keywords: contracts, gradual typing, hybrid typing, blame calculus}
}
Document
Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development
Abstract
Many of today's programming languages are broken. Poor performance, lack of features and hard-to-reason-about semantics can cost dearly in software maintenance and inefficient execution. The problem is only getting worse with programming languages proliferating and hardware becoming more complicated. An important reason for this brokenness is that much of language design is implementation-driven. The difficulties in implementation and insufficient understanding of concepts bake bad designs into the language itself. Concurrency, architectural details and garbage collection are three fundamental concerns that contribute much to the complexities of implementing managed languages.
We propose the micro virtual machine, a thin abstraction designed specifically to relieve implementers of managed languages of the most fundamental implementation challenges that currently impede good design. The micro virtual machine targets abstractions over memory (garbage collection), architecture (compiler backend), and concurrency. We motivate the micro virtual machine and give an account of the design and initial experience of a concrete instance, which we call Mu, built over a two year period. Our goal is to remove an important barrier to performant and semantically sound managed language design and implementation.
Cite as
Kunshan Wang, Yi Lin, Stephen M. Blackburn, Michael Norrish, and Antony L. Hosking. Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 321-336, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.SNAPL.2015.321,
author = {Wang, Kunshan and Lin, Yi and Blackburn, Stephen M. and Norrish, Michael and Hosking, Antony L.},
title = {{Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {321--336},
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.321},
URN = {urn:nbn:de:0030-drops-50341},
doi = {10.4230/LIPIcs.SNAPL.2015.321},
annote = {Keywords: virtual machines, concurrency, just-in-time compiling, garbage collection}
}