Volume
LIPIcs, Volume 71
2nd Summit on Advances in Programming Languages (SNAPL 2017)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Summit on Advances in Programming Languages (SNAPL)
Event
SNAPL 2017, May 7-10, 2017, Asilomar, CA, USAEditors
Publication Details
- published at: 2017-05-05
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-032-3
- DBLP: db/conf/snapl/snapl2017
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 71, SNAPL'17, Complete Volume
Abstract
LIPIcs, Volume 71, SNAPL'17, Complete Volume
Cite as
2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Proceedings{lerner_et_al:LIPIcs.SNAPL.2017,
title = {{LIPIcs, Volume 71, SNAPL'17, Complete Volume}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
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},
URN = {urn:nbn:de:0030-drops-71379},
doi = {10.4230/LIPIcs.SNAPL.2017},
annote = {Keywords: Programming Languages}
}
Document
Front Matter
Front Matter, Table of Contents, Preface
Abstract
Front Matter, Table of Contents, Preface
Cite as
2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{lerner_et_al:LIPIcs.SNAPL.2017.0,
author = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
title = {{Front Matter, Table of Contents, Preface}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {0:i--0:viii},
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.0},
URN = {urn:nbn:de:0030-drops-71160},
doi = {10.4230/LIPIcs.SNAPL.2017.0},
annote = {Keywords: Front Matter, Table of Contents, Preface}
}
Document
Everest: Towards a Verified, Drop-in Replacement of HTTPS
Abstract
The HTTPS ecosystem is the foundation on which Internet security is built. At the heart of this ecosystem is the Transport Layer Security (TLS) protocol, which in turn uses the X.509 public-key infrastructure and numerous cryptographic constructions and algorithms. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks and emergency patches many times a year. We describe our ongoing efforts in Everest (The Everest VERified End-to-end Secure Transport) a project that aims to build and deploy a verified version of TLS and other components of HTTPS, replacing the current infrastructure with proven, secure software.
Aiming both at full verification and usability, we conduct high-level code-based, game-playing proofs of security on cryptographic implementations that yield efficient, deployable code, at the level of C and assembly. Concretely, we use F*, a dependently typed language for programming, meta-programming, and proving at a high level, while relying on low-level DSLs embedded within F* for programming low-level components when necessary for performance and, sometimes, side-channel resistance. To compose the pieces, we compile all our code to source-like C and assembly, suitable for deployment and integration with existing code bases, as well as audit by independent security experts.
Our main results so far include (1) the design of Low*, a subset of F* designed for C-like imperative programming but with high-level verification support, and KreMLin, a compiler that extracts Low* programs to C; (2) an implementation of the TLS-1.3 record layer in Low*, together with a proof of its concrete cryptographic security; (3) Vale, a new DSL for verified assembly language, and several optimized cryptographic primitives proven functionally correct and side-channel resistant. In an early deployment, all our verified software is integrated and deployed within libcurl, a widely used library of networking protocols.
Cite as
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 1:1-1:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bhargavan_et_al:LIPIcs.SNAPL.2017.1,
author = {Bhargavan, Karthikeyan and Bond, Barry and Delignat-Lavaud, Antoine and Fournet, C\'{e}dric and Hawblitzel, Chris and Hritcu, Catalin and Ishtiaq, Samin and Kohlweiss, Markulf and Leino, Rustan and Lorch, Jay and Maillard, Kenji and Pan, Jianyang and Parno, Bryan and Protzenko, Jonathan and Ramananandro, Tahina and Rane, Ashay and Rastogi, Aseem and Swamy, Nikhil and Thompson, Laure and Wang, Peng and Zanella-B\'{e}guelin, Santiago and Zinzindohou\'{e}, Jean-Karim},
title = {{Everest: Towards a Verified, Drop-in Replacement of HTTPS}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {1:1--1:12},
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.1},
URN = {urn:nbn:de:0030-drops-71196},
doi = {10.4230/LIPIcs.SNAPL.2017.1},
annote = {Keywords: Security, Cryptography, Verification, TLS}
}
Document
Domain-Specific Symbolic Compilation
Abstract
A symbolic compiler translates a program to symbolic constraints, automatically reducing model checking and synthesis to constraint solving. We show that new applications of constraint solving require domain-specific encodings that yield the required orders of magnitude improvements in solver efficiency. Unfortunately, these encodings cannot be obtained with today's symbolic compilation.
We introduce symbolic languages that encapsulate domain-specific encodings under abstractions that behave as their non-symbolic counterparts: client code using the abstractions can be tested and debugged on concrete inputs. When client code is symbolically compiled, the resulting constraints use domain-specific encodings.
We demonstrate the idea on the first fully symbolic checker of type systems; a program partitioner; and a parallelizer of tree computations. In each of these case studies, symbolic languages improved on classical symbolic compilers by orders of magnitude.
Cite as
Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, and Nathaniel Yazdani. Domain-Specific Symbolic Compilation. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bodik_et_al:LIPIcs.SNAPL.2017.2,
author = {Bod{\'\i}k, Rastislav and Chandra, Kartik and Phothilimthana, Phitchaya Mangpo and Yazdani, Nathaniel},
title = {{Domain-Specific Symbolic Compilation}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {2:1--2:17},
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.2},
URN = {urn:nbn:de:0030-drops-71334},
doi = {10.4230/LIPIcs.SNAPL.2017.2},
annote = {Keywords: Symbolic evaluation, program synthesis, DSLs}
}
Document
The End of History? Using a Proof Assistant to Replace Language Design with Library Design
Abstract
Functionality of software systems has exploded in part because of advances in programming-language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodges of command-line tools. Domain-specific languages may be viewed as an evolution of the power of reusable interfaces, when those interfaces become so flexible as to deserve to be called programming languages. However, common approaches to domain-specific languages give up many of the hard-won advantages of library-building in a rich common language, and even the traditional approach poses significant challenges in learning new APIs. We suggest that instead of continuing to develop new domain-specific languages, our community should embrace library-based ecosystems within very expressive languages that mix programming and theorem proving. Our prototype framework Fiat, a library for the Coq proof assistant, turns languages into easily comprehensible libraries via the key idea of modularizing functionality and performance away from each other, the former via macros that desugar into higher-order logic and the latter via optimization scripts that derive efficient code from logical programs.
Cite as
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, and Katherine Ye. The End of History? Using a Proof Assistant to Replace Language Design with Library Design. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{chlipala_et_al:LIPIcs.SNAPL.2017.3,
author = {Chlipala, Adam and Delaware, Benjamin and Duchovni, Samuel and Gross, Jason and Pit-Claudel, Cl\'{e}ment and Suriyakarn, Sorawit and Wang, Peng and Ye, Katherine},
title = {{The End of History? Using a Proof Assistant to Replace Language Design with Library Design}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {3:1--3: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.3},
URN = {urn:nbn:de:0030-drops-71233},
doi = {10.4230/LIPIcs.SNAPL.2017.3},
annote = {Keywords: Domain-specific languages, synthesis, verification, proof assistants, software development}
}
Document
Natural Language is a Programming Language: Applying Natural Language Processing to Software Development
Abstract
A powerful, but limited, way to view software is as source code alone. Treating a program as a sequence of instructions enables it to be formalized and makes it amenable to mathematical techniques such as abstract interpretation and model checking.
A program consists of much more than a sequence of instructions. Developers make use of test cases, documentation, variable names, program structure, the version control repository, and more. I argue that it is time to take the blinders off of software analysis tools: tools should use all these artifacts to deduce more powerful and useful information about the program.
Researchers are beginning to make progress towards this vision. This paper gives, as examples, four results that find bugs and generate code by applying natural language processing techniques to software artifacts. The four techniques use as input error messages, variable names, procedure documentation, and user questions. They use four different NLP techniques: document similarity, word semantics, parse trees, and neural networks.
The initial results suggest that this is a promising avenue for future work.
Cite as
Michael D. Ernst. Natural Language is a Programming Language: Applying Natural Language Processing to Software Development. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 4:1-4:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{ernst:LIPIcs.SNAPL.2017.4,
author = {Ernst, Michael D.},
title = {{Natural Language is a Programming Language: Applying Natural Language Processing to Software Development}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {4:1--4:14},
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.4},
URN = {urn:nbn:de:0030-drops-71357},
doi = {10.4230/LIPIcs.SNAPL.2017.4},
annote = {Keywords: natural language processing, program analysis, software development}
}
Document
Fission: Secure Dynamic Code-Splitting for JavaScript
Abstract
Traditional web programming involves the creation of two distinct programs: a client-side front-end, a server-side back-end, and a lot of communications boilerplate. An alternative approach is to use a tierless programming model, where a single program describes the behavior of both the client and the server, and the runtime system takes care of communication. Unfortunately, this usually entails adopting a new language and thus abandoning well-worn libraries and web programming tools.
In this paper, we present our ongoing work on Fission, a platform that uses dynamic tier-splitting and dynamic information flow control to transparently run a single JavaScript program across the client and server. Although static tier-splitting has been studied before, our focus on dynamic approaches presents several new challenges and opportunities. For example, Fission supports characteristic JavaScript features such as eval and sophisticated JavaScript libraries like React. Therefore, programmers can reason about the integrity and confidentiality of information while continuing to use common libraries and programming patterns. Moreover, by unifying the client and server into a single program, Fission allows language-based tools, like type systems and IDEs, to manipulate complete web applications. To illustrate, we use TypeScript to ensure that client-server communication does not go wrong.
Cite as
Arjun Guha, Jean-Baptiste Jeannin, Rachit Nigam, Jane Tangen, and Rian Shambaugh. Fission: Secure Dynamic Code-Splitting for JavaScript. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{guha_et_al:LIPIcs.SNAPL.2017.5,
author = {Guha, Arjun and Jeannin, Jean-Baptiste and Nigam, Rachit and Tangen, Jane and Shambaugh, Rian},
title = {{Fission: Secure Dynamic Code-Splitting for JavaScript}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {5:1--5:13},
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.5},
URN = {urn:nbn:de:0030-drops-71247},
doi = {10.4230/LIPIcs.SNAPL.2017.5},
annote = {Keywords: JavaScript, information flow control}
}
Document
I Can Parse You: Grammars for Dialogs
Abstract
Humans and computers increasingly converse via natural language. Those conversations are moving from today's simple question answering and command-and-control to more complex dialogs. Developers must specify those dialogs. This paper explores how to assist developers in this specification. We map out the staggering variety of applications for human-computer dialogs and distill it into a catalog of flow patterns. Based on that, we articulate the requirements for dialog programming models and offer our vision for satisfying these requirements using grammars. If our approach catches on, computers will soon parse you to better assist you in your daily life.
Cite as
Martin Hirzel, Louis Mandel, Avraham Shinnar, Jerome Simeon, and Mandana Vaziri. I Can Parse You: Grammars for Dialogs. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{hirzel_et_al:LIPIcs.SNAPL.2017.6,
author = {Hirzel, Martin and Mandel, Louis and Shinnar, Avraham and Simeon, Jerome and Vaziri, Mandana},
title = {{I Can Parse You: Grammars for Dialogs}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {6:1--6: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.6},
URN = {urn:nbn:de:0030-drops-71180},
doi = {10.4230/LIPIcs.SNAPL.2017.6},
annote = {Keywords: Bots, virtual agents, dialog managers, domain-specific languages}
}
Document
Leveraging Sequential Computation for Programming Efficient and Reliable Distributed Systems
Abstract
While sequential programs represent a simple and natural form for expressing functionality, corresponding distributed implementations get considerably more complex. We examine the possibility of using the sequential computation model for programming distributed systems and requirements for making that possible. The benefits of such an approach include easier specification and reasoning about behaviors in the system, as well as a possibility to directly reuse existing techniques for checking correctness and optimization of sequential programs to produce efficient and reliable distributed implementations.
Cite as
Ivan Kuraj and Armando Solar-Lezama. Leveraging Sequential Computation for Programming Efficient and Reliable Distributed Systems. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kuraj_et_al:LIPIcs.SNAPL.2017.7,
author = {Kuraj, Ivan and Solar-Lezama, Armando},
title = {{Leveraging Sequential Computation for Programming Efficient and Reliable Distributed Systems}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {7:1--7: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.7},
URN = {urn:nbn:de:0030-drops-71321},
doi = {10.4230/LIPIcs.SNAPL.2017.7},
annote = {Keywords: distributed systems, sequential computation, verification}
}
Document
Intermittent Computing: Challenges and Opportunities
Abstract
The maturation of energy-harvesting technology and ultra-low-power computer systems has led to the advent of intermittently-powered, batteryless devices that operate entirely using energy extracted from their environment. Intermittently operating devices present a rich vein of programming languages research challenges and the purpose of this paper is to illustrate these challenges to the PL research community. To provide depth, this paper includes a survey of the hardware and software design space of intermittent computing platforms. On the foundation of these research challenges and the state of the art in intermittent hardware and software, this paper describes several future PL research directions, emphasizing a connection between intermittence, distributed computing, energy-aware programming and compilation, and approximate computing. We illustrate these connections with a discussion of our ongoing work on programming for intermittence, and on building and simulating intermittent distributed systems.
Cite as
Brandon Lucia, Vignesh Balaji, Alexei Colin, Kiwan Maeng, and Emily Ruppel. Intermittent Computing: Challenges and Opportunities. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{lucia_et_al:LIPIcs.SNAPL.2017.8,
author = {Lucia, Brandon and Balaji, Vignesh and Colin, Alexei and Maeng, Kiwan and Ruppel, Emily},
title = {{Intermittent Computing: Challenges and Opportunities}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {8:1--8:14},
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.8},
URN = {urn:nbn:de:0030-drops-71314},
doi = {10.4230/LIPIcs.SNAPL.2017.8},
annote = {Keywords: Intermittent computing, Energy-harvesting devices}
}
Document
Uncanny Valleys in Declarative Language Design
Abstract
When people write programs in conventional programming languages, they over-specify how to solve the problem they have in mind. Over-specification prevents the language's implementation from making many optimization decisions, leaving programmers with this burden. In more declarative languages, programmers over-specify less, enabling the implementation to make more choices for them. As these decisions improve, programmers shift more attention from implementation to their real problems. This process easily overshoots. When under-specified programs almost always work well enough, programmers rarely need to think about implementation details. As their understanding of implementation choices atrophies, the controls provided so they can override these decisions become obscure.
Our declarative language project, Yedalog, is in the midst of this dilemma. The improvements in question make our users more productive, so we cannot simply retreat back towards over-specification. To proceed forward instead, we must meet some of the expectations we prematurely provoked, and our implementation's behavior must help users learn expectations more aligned with our intended semantics.
These are general issues. Discussing their concrete manifestation in Yedalog should help other declarative systems that come to face these issues.
Cite as
Mark S. Miller, Daniel von Dincklage, Vuk Ercegovac, and Brian Chin. Uncanny Valleys in Declarative Language Design. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 9:1-9:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{miller_et_al:LIPIcs.SNAPL.2017.9,
author = {Miller, Mark S. and von Dincklage, Daniel and Ercegovac, Vuk and Chin, Brian},
title = {{Uncanny Valleys in Declarative Language Design}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {9:1--9:12},
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.9},
URN = {urn:nbn:de:0030-drops-71299},
doi = {10.4230/LIPIcs.SNAPL.2017.9},
annote = {Keywords: Declarative logic programming language}
}
Document
Programming Language Tools and Techniques for 3D Printing
Abstract
We propose a research agenda to investigate programming language techniques for improving affordable, end-user desktop manufacturing processes such as 3D printing. Our goal is to adapt programming languages tools and extend the decades of research in industrial, high-end CAD/CAM in order to help make affordable desktop manufacturing processes more accurate, fast, reliable, and accessible to end-users. We focus on three major areas where 3D printing can benefit from programming language tools: design synthesis, optimizing compilation, and runtime monitoring. We present preliminary results on synthesizing editable CAD models from difficult-to-edit surface meshes, discuss potential new compilation strategies, and propose runtime monitoring techniques. We conclude by discussing additional near-future directions we intend to pursue.
Cite as
Chandrakana Nandi, Anat Caspi, Dan Grossman, and Zachary Tatlock. Programming Language Tools and Techniques for 3D Printing. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 10:1-10:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{nandi_et_al:LIPIcs.SNAPL.2017.10,
author = {Nandi, Chandrakana and Caspi, Anat and Grossman, Dan and Tatlock, Zachary},
title = {{Programming Language Tools and Techniques for 3D Printing}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {10:1--10:12},
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.10},
URN = {urn:nbn:de:0030-drops-71226},
doi = {10.4230/LIPIcs.SNAPL.2017.10},
annote = {Keywords: 3D printing, rapid prototyping, desktop manufacturing, compilers, verification, synthesis}
}
Document
Toward Semantic Foundations for Program Editors
Abstract
Programming language definitions assign formal meaning to complete programs. Programmers, however, spend a substantial amount of time interacting with incomplete programs - programs with holes, type inconsistencies and binding inconsistencies - using tools like program editors and live programming environments (which interleave editing and evaluation). Semanticists have done comparatively little to formally characterize (1) the static and dynamic semantics of incomplete programs; (2) the actions available to programmers as they edit and inspect incomplete programs; and (3) the behavior of editor services that suggest likely edit actions to the programmer based on semantic information extracted from the incomplete program being edited, and from programs that the system has encountered in the past.
This paper serves as a vision statement for a research program that seeks to develop these "missing" semantic foundations. Our hope is that these contributions, which will take the form of a series of simple formal calculi equipped with a tractable metatheory, will guide the design of a variety of current and future interactive programming tools, much as various lambda calculi have guided modern language designs. Our own research will apply these principles in the design of Hazel, an experimental live lab notebook programming environment designed for data science tasks. We plan to co-design the Hazel language with the editor so that we can explore concepts such as edit-time semantic conflict resolution mechanisms and mechanisms that allow library providers to install library-specific editor services.
Cite as
Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. Toward Semantic Foundations for Program Editors. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{omar_et_al:LIPIcs.SNAPL.2017.11,
author = {Omar, Cyrus and Voysey, Ian and Hilton, Michael and Sunshine, Joshua and Le Goues, Claire and Aldrich, Jonathan and Hammer, Matthew A.},
title = {{Toward Semantic Foundations for Program Editors}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {11:1--11:12},
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.11},
URN = {urn:nbn:de:0030-drops-71273},
doi = {10.4230/LIPIcs.SNAPL.2017.11},
annote = {Keywords: program editors, type systems, live programming, program prediction}
}
Document
Linking Types for Multi-Language Software: Have Your Cake and Eat It Too
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
Teaching Programming Languages by Experimental and Adversarial Thinking
Abstract
We present a new approach to teaching programming language courses. Its essence is to view programming language learning as a natural science activity, where students probe languages experimentally to understand both the normal and extreme behaviors of their features. This has natural parallels to the "security mindset" of computer security, with languages taking the place of servers and other systems. The approach is modular (with minimal dependencies), incremental (it can be introduced slowly into existing classes), interoperable (it does not need to push out other, existing methods), and complementary (since it introduces a new mode of thinking).
Cite as
Justin Pombrio, Shriram Krishnamurthi, and Kathi Fisler. Teaching Programming Languages by Experimental and Adversarial Thinking. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 13:1-13:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{pombrio_et_al:LIPIcs.SNAPL.2017.13,
author = {Pombrio, Justin and Krishnamurthi, Shriram and Fisler, Kathi},
title = {{Teaching Programming Languages by Experimental and Adversarial Thinking}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {13:1--13:9},
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.13},
URN = {urn:nbn:de:0030-drops-71178},
doi = {10.4230/LIPIcs.SNAPL.2017.13},
annote = {Keywords: mystery languages, interpreters, paradigms, education}
}
Document
Let's Fix OpenGL
Abstract
From windowing systems to virtual reality, real-time graphics code is ubiquitous. Programming models for constructing graphics software, however, have largely escaped the attention of programming languages researchers. This essay introduces the programming model of OpenGL, a ubiquitous API for real-time graphics applications, for a language-oriented audience. It highlights six broad problems with the programming model and connects them to traditions in PL research. The issues range from classic pitfalls, where established thinking can apply, to new open problems, where novel research is needed.
Cite as
Adrian Sampson. Let's Fix OpenGL. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 14:1-14:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{sampson:LIPIcs.SNAPL.2017.14,
author = {Sampson, Adrian},
title = {{Let's Fix OpenGL}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {14:1--14:12},
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.14},
URN = {urn:nbn:de:0030-drops-71305},
doi = {10.4230/LIPIcs.SNAPL.2017.14},
annote = {Keywords: language design, real-time graphics, OpenGL, GPUs, heterogeneity}
}
Document
Search for Program Structure
Abstract
The community of programming language research loves the Curry-Howard correspondence between proofs and programs. Cut-elimination as computation, theorems for free, 'call/cc' as excluded middle, dependently typed languages as proof assistants, etc.
Yet we have, for all these years, missed an obvious observation: "the structure of programs corresponds to the structure of proof search". For pure programs and intuitionistic logic, more is known about the latter than the former. We think we know what programs are, but logicians know better!
To motivate the study of proof search for program structure, we retrace recent research on applying focusing to study the canonical structure of simply-typed lambda-terms. We then motivate the open problem of extending canonical forms to support richer type systems, such as polymorphism, by discussing a few enticing applications of more canonical program representations.
Cite as
Gabriel Scherer. Search for Program Structure. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{scherer:LIPIcs.SNAPL.2017.15,
author = {Scherer, Gabriel},
title = {{Search for Program Structure}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {15:1--15:14},
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.15},
URN = {urn:nbn:de:0030-drops-71346},
doi = {10.4230/LIPIcs.SNAPL.2017.15},
annote = {Keywords: programs, proofs, focusing, canonicity}
}
Document
AP: Artificial Programming
Abstract
The ability to automatically discover a program consistent with a given user intent (specification) is the holy grail of Computer Science. While significant progress has been made on the so-called problem of Program Synthesis, a number of challenges remain; particularly for the case of synthesizing richer and larger programs. This is in large part due to the difficulty of search over the space of programs. In this paper, we argue that the above-mentioned challenge can be tackled by learning synthesizers automatically from a large amount of training data. We present a first step in this direction by describing our novel synthesis approach based on two neural architectures for tackling the two key challenges of Learning to understand partial input-output specifications and Learning to search programs. The first neural architecture called the Spec Encoder computes a continuous representation of the specification, whereas the second neural architecture called the Program Generator incrementally constructs programs in a hypothesis space that is conditioned by the specification vector. The key idea of the approach is to train these architectures using a large set of (spec,P) pairs, where P denotes a program sampled from the DSL L and spec denotes the corresponding specification satisfied by P. We demonstrate the effectiveness of our approach on two preliminary instantiations. The first instantiation, called Neural FlashFill, corresponds to the domain of string manipulation programs similar to that of FlashFill. The second domain considers string transformation programs consisting of composition of API functions. We show that a neural system is able to perform quite well in learning a large majority of programs from few input-output examples. We believe this new approach will not only dramatically expand the applicability and effectiveness of Program Synthesis, but also would lead to the coming together of the Program Synthesis and Machine Learning research disciplines.
Cite as
Rishabh Singh and Pushmeet Kohli. AP: Artificial Programming. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 16:1-16:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{singh_et_al:LIPIcs.SNAPL.2017.16,
author = {Singh, Rishabh and Kohli, Pushmeet},
title = {{AP: Artificial Programming}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {16:1--16:12},
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.16},
URN = {urn:nbn:de:0030-drops-71284},
doi = {10.4230/LIPIcs.SNAPL.2017.16},
annote = {Keywords: Neural Program Synthesis, Neural Programming, Neural FlashFill}
}
Document
Migratory Typing: Ten Years Later
Abstract
In this day and age, many developers work on large, untyped code repositories. Even if they are the creators of the code, they notice that they have to figure out the equivalent of method signatures every time they work on old code. This step is time consuming and error prone.
Ten years ago, the two lead authors outlined a linguistic solution to this problem. Specifically they proposed the creation of typed twins for untyped programming languages so that developers could migrate scripts from the untyped world to a typed one in an incremental manner. Their programmatic paper also spelled out three guiding design principles concerning the acceptance of grown idioms, the soundness of mixed-typed programs, and the units of migration.
This paper revisits this idea of a migratory type system as implemented for Racket. It explains how the design principles have been used to produce the Typed Racket twin and presents an assessment of the project's status, highlighting successes and failures.
Cite as
Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. Migratory Typing: Ten Years Later. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{tobinhochstadt_et_al:LIPIcs.SNAPL.2017.17,
author = {Tobin-Hochstadt, Sam and Felleisen, Matthias and Findler, Robert and Flatt, Matthew and Greenman, Ben and Kent, Andrew M. and St-Amour, Vincent and Strickland, T. Stephen and Takikawa, Asumu},
title = {{Migratory Typing: Ten Years Later}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {17:1--17:17},
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.17},
URN = {urn:nbn:de:0030-drops-71202},
doi = {10.4230/LIPIcs.SNAPL.2017.17},
annote = {Keywords: design principles, type systems, gradual typing}
}
Document
Taming the Static Analysis Beast
Abstract
While industrial-strength static analysis over large, real-world codebases has become commonplace, so too have difficult-to-analyze language constructs, large libraries, and popular frameworks. These features make constructing and evaluating a novel, sound analysis painful, error-prone, and tedious. We motivate the need for research to address these issues by highlighting some of the many challenges faced by static analysis developers in today's software ecosystem. We then propose our short- and long-term research agenda to make static analysis over modern software less burdensome.
Cite as
John Toman and Dan Grossman. Taming the Static Analysis Beast. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{toman_et_al:LIPIcs.SNAPL.2017.18,
author = {Toman, John and Grossman, Dan},
title = {{Taming the Static Analysis Beast}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {18:1--18:14},
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.18},
URN = {urn:nbn:de:0030-drops-71213},
doi = {10.4230/LIPIcs.SNAPL.2017.18},
annote = {Keywords: static analysis, frameworks, api knowledge, library specifications}
}
Document
Programming Language Abstractions for Modularly Verified Distributed Systems
Abstract
Distributed systems are rarely developed as monolithic programs. Instead, like any software, these systems may consist of multiple program components, which are then compiled separately and linked together. Modern systems also incorporate various services interacting with each other and with client applications. However, state-of-the-art verification tools focus predominantly on verifying standalone, closed-world protocols or systems, thus failing to account for the compositional nature of distributed systems. For example, standalone verification has the drawback that when protocols and their optimized implementations evolve, one must re-verify the entire system from scratch, instead of leveraging compositionality to contain the reverification effort.
In this paper, we focus on the challenge of modular verification of distributed systems with respect to high-level protocol invariants as well as for low-level implementation safety properties. We argue that the missing link between the two is a programming paradigm that would allow one to reason about both high-level distributed protocols and low-level implementation primitives in a single verification-friendly framework. Such a link would make it possible to reap the benefits from both the vast body of research in distributed computing, focused on modular protocol decomposition and consistency properties, as well as from the recent advances in program verification, enabling construction of provably correct systems implementations. To showcase the modular verification challenges, we present some typical scenarios of decomposition between a distributed protocol and its implementations. We then describe our ongoing research agenda, in which we are attempting to address the outlined problems by providing a typing discipline and a set of domain-specific primitives for specifying, implementing and verifying distributed systems. Our approach, mechanized within a proof assistant, provides the means of decomposition necessary for modular proofs about distributed protocols and systems.
Cite as
James R. Wilcox, Ilya Sergey, and Zachary Tatlock. Programming Language Abstractions for Modularly Verified Distributed Systems. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 19:1-19:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{wilcox_et_al:LIPIcs.SNAPL.2017.19,
author = {Wilcox, James R. and Sergey, Ilya and Tatlock, Zachary},
title = {{Programming Language Abstractions for Modularly Verified Distributed Systems}},
booktitle = {2nd Summit on Advances in Programming Languages (SNAPL 2017)},
pages = {19:1--19:12},
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.19},
URN = {urn:nbn:de:0030-drops-71266},
doi = {10.4230/LIPIcs.SNAPL.2017.19},
annote = {Keywords: Distributed systems, program verification, distributed protocols, domain-specific languages, type systems, dependent types, program logics.}
}