16 Search Results for "Bodík, Rastislav"

Volume

LIPIcs, Volume 136

3rd Summit on Advances in Programming Languages (SNAPL 2019)

SNAPL 2019, May 16-17, 2019, Providence, RI, USA

Editors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Volume

LIPIcs, Volume 71

2nd Summit on Advances in Programming Languages (SNAPL 2017)

SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA

Editors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Document
DOI: 10.4230/LIPIcs.CSL.2026.40
The Groupoid-Syntax of Type Theory Is a Set

Authors: Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.
Cite as

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
  title =	{{The Groupoid-Syntax of Type Theory Is a Set}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{40:1--40:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
  URN =		{urn:nbn:de:0030-drops-254650},
  doi =		{10.4230/LIPIcs.CSL.2026.40},
  annote =	{Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.7
Modern Datalog: Concepts, Methods, Applications (Invited Paper)

Authors: Markus Krötzsch

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract
Pure Datalog is arguably the most fundamental rule language, elegant and simple, but also often too limited to be useful in practice. This has motivated the introduction of many new expressive features, ranging from datatypes and related functions, over aggregates and semi-ring generalisations, to existential quantifiers and complex terms. In spite of their variety, all these approaches remain true to the nature of Datalog as a direct, pattern-based way of computing on structured data. We therefore find that a modern notion of Datalog is emerging, distinctly different from other approaches of logic programming and with its own set of related methods and applications. In this course, we introduce Datalog and its most common extensions, and explain when and how these features can be used together (which is often, but not always, safe to do). We further look at modern Datalog systems and some of their primary use cases. Hands-on work with Datalog and its extensions is done with the free Datalog engine https://knowsys.github.io/nemo-doc/. The course is accessible to all audiences and does not assume specific prior knowledge.
Cite as

Markus Krötzsch. Modern Datalog: Concepts, Methods, Applications (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 7:1-7:41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{krotzsch:OASIcs.RW.2024/2025.7,
  author =	{Kr\"{o}tzsch, Markus},
  title =	{{Modern Datalog: Concepts, Methods, Applications}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{7:1--7:41},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.7},
  URN =		{urn:nbn:de:0030-drops-250524},
  doi =		{10.4230/OASIcs.RW.2024/2025.7},
  annote =	{Keywords: Datalog, query language, knowlegde representation and reasoning, logic programming, Horn logic, SPARQL, datatypes and aggregation, lecture notes, tutorial}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.56
Negated String Containment Is Decidable

Authors: Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate ¬Contains(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.
Cite as

Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. Negated String Containment Is Decidable. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 56:1-56:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.MFCS.2025.56,
  author =	{Havlena, Vojt\v{e}ch and He\v{c}ko, Michal and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej},
  title =	{{Negated String Containment Is Decidable}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{56:1--56:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.56},
  URN =		{urn:nbn:de:0030-drops-241631},
  doi =		{10.4230/LIPIcs.MFCS.2025.56},
  annote =	{Keywords: not-contains, string constraints, word combinatorics, primitive word}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.92
Fully Dynamic Algorithms for Transitive Reduction

Authors: Gramoz Goranci, Adam Karczmarz, Ali Momeni, and Nikos Parotsidis

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Given a directed graph G, a transitive reduction G^t of G (first studied by Aho, Garey, Ullman [SICOMP `72]) is a minimal subgraph of G that preserves the reachability relation between every two vertices in G. In this paper, we study the computational complexity of transitive reduction in the dynamic setting. We obtain the first fully dynamic algorithms for maintaining a transitive reduction of a general directed graph undergoing updates such as edge insertions or deletions. Our first algorithm achieves O(m+n log n) amortized update time, which is near-optimal for sparse directed graphs, and can even support extended update operations such as inserting a set of edges all incident to the same vertex, or deleting an arbitrary set of edges. Our second algorithm relies on fast matrix multiplication and achieves O(m+ n^{1.585}) worst-case update time.
Cite as

Gramoz Goranci, Adam Karczmarz, Ali Momeni, and Nikos Parotsidis. Fully Dynamic Algorithms for Transitive Reduction. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 92:1-92:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{goranci_et_al:LIPIcs.ICALP.2025.92,
  author =	{Goranci, Gramoz and Karczmarz, Adam and Momeni, Ali and Parotsidis, Nikos},
  title =	{{Fully Dynamic Algorithms for Transitive Reduction}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{92:1--92:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.92},
  URN =		{urn:nbn:de:0030-drops-234697},
  doi =		{10.4230/LIPIcs.ICALP.2025.92},
  annote =	{Keywords: Spectral sparsification, Dynamic algorithms, (Directed) hypergraphs, Data structures}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.10
Bottom-Up Synthesis of Memory Mutations with Separation Logic

Authors: Kasra Ferdowsi and Hila Peleg

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Programming-by-Example (PBE) is the paradigm of program synthesis specified via input-output pairs. It is commonly used because examples are easy to provide and collect from the environment. A popular optimization for enumerative synthesis with examples is Observational Equivalence (OE), which groups programs into equivalence classes according to their evaluation on example inputs. Current formulations of OE, however, are severely limited by the assumption that the synthesizer’s target language contains only pure components with no side-effects, either enforcing this in their target language, or ignoring it, leading to an incorrect enumeration. This limits their ability to use realistic component sets. We address this limitation by borrowing from Separation Logic, which can compositionally reason about heap mutations. We reformulate PBE using a restricted Separation Logic: Concrete Heap Separation Logic (CHSL), transforming the search for programs into a proof search in CHSL. This lets us perform bottom-up enumerative synthesis without the need for expert-provided annotations or domain-specific inferences, but with three key advantages: we (i) preserve correctness in the presence of memory-mutating operations, (ii) compact the search space by representing many concrete programs as one under CHSL, and (iii) perform a provably correct OE-reduction. We present SObEq (Side-effects in OBservational EQuivalence), a bottom-up enumerative algorithm that, given a PBE task, searches for its CHSL derivation. The SObEq algorithm is proved correct with no purity assumptions: we show it is guaranteed to lose no solutions. We also evaluate our implementation of SObEq on benchmarks from the literature and online sources, and show that it produces high-quality results quickly.
Cite as

Kasra Ferdowsi and Hila Peleg. Bottom-Up Synthesis of Memory Mutations with Separation Logic. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferdowsi_et_al:LIPIcs.ECOOP.2025.10,
  author =	{Ferdowsi, Kasra and Peleg, Hila},
  title =	{{Bottom-Up Synthesis of Memory Mutations with Separation Logic}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{10:1--10:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.10},
  URN =		{urn:nbn:de:0030-drops-233036},
  doi =		{10.4230/LIPIcs.ECOOP.2025.10},
  annote =	{Keywords: Program synthesis, observational equivalence}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.4
Learning Aggregate Queries Defined by First-Order Logic with Counting

Authors: Steffen van Bergerem and Nicole Schweikardt

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
In the logical framework introduced by Grohe and Turán (TOCS 2004) for Boolean classification problems, the instances to classify are tuples from a logical structure, and Boolean classifiers are described by parametric models based on logical formulas. This is a specific scenario for supervised passive learning, where classifiers should be learned based on labelled examples. Existing results in this scenario focus on Boolean classification. This paper presents learnability results beyond Boolean classification. We focus on multiclass classification problems where the task is to assign input tuples to arbitrary integers. To represent such integer-valued classifiers, we use aggregate queries specified by an extension of first-order logic with counting terms called FOC₁. Our main result shows the following: given a database of polylogarithmic degree, within quasi-linear time, we can build an index structure that makes it possible to learn FOC₁-definable integer-valued classifiers in time polylogarithmic in the size of the database and polynomial in the number of training examples.
Cite as

Steffen van Bergerem and Nicole Schweikardt. Learning Aggregate Queries Defined by First-Order Logic with Counting. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.ICDT.2025.4,
  author =	{van Bergerem, Steffen and Schweikardt, Nicole},
  title =	{{Learning Aggregate Queries Defined by First-Order Logic with Counting}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.4},
  URN =		{urn:nbn:de:0030-drops-229457},
  doi =		{10.4230/LIPIcs.ICDT.2025.4},
  annote =	{Keywords: Supervised learning, multiclass classification problems, counting logic}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2019
LIPIcs, Volume 136, SNAPL'19, Complete Volume

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
LIPIcs, Volume 136, SNAPL'19, Complete Volume
Cite as

3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Proceedings{lerner_et_al:LIPIcs.SNAPL.2019,
  title =	{{LIPIcs, Volume 136, SNAPL'19, Complete Volume}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  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.2019},
  URN =		{urn:nbn:de:0030-drops-108657},
  doi =		{10.4230/LIPIcs.SNAPL.2019},
  annote =	{Keywords: Software and its engineering, General programming languages, Semantics}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.SNAPL.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lerner_et_al:LIPIcs.SNAPL.2019.0,
  author =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  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.2019.0},
  URN =		{urn:nbn:de:0030-drops-105439},
  doi =		{10.4230/LIPIcs.SNAPL.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2019.10
Toward Domain-Specific Solvers for Distributed Consistency

Authors: Lindsey Kuper and Peter Alvaro

Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)

Abstract
To guard against machine failures, modern internet services store multiple replicas of the same application data within and across data centers, which introduces the problem of keeping geo-distributed replicas consistent with one another in the face of network partitions and unpredictable message latency. To avoid costly and conservative synchronization protocols, many real-world systems provide only weak consistency guarantees (e.g., eventual, causal, or PRAM consistency), which permit certain kinds of disagreement among replicas. There has been much recent interest in language support for specifying and verifying such consistency properties. Although these properties are usually beyond the scope of what traditional type checkers or compiler analyses can guarantee, solver-aided languages are up to the task. Inspired by systems like Liquid Haskell [Vazou et al., 2014] and Rosette [Torlak and Bodik, 2014], we believe that close integration between a language and a solver is the right path to consistent-by-construction distributed applications. Unfortunately, verifying distributed consistency properties requires reasoning about transitive relations (e.g., causality or happens-before), partial orders (e.g., the lattice of replica states under a convergent merge operation), and properties relevant to message processing or API invocation (e.g., commutativity and idempotence) that cannot be easily or efficiently carried out by general-purpose SMT solvers that lack native support for this kind of reasoning. We argue that domain-specific SMT-based tools that exploit the mathematical foundations of distributed consistency would enable both more efficient verification and improved ease of use for domain experts. The principle of exploiting domain knowledge for efficiency and expressivity that has borne fruit elsewhere - such as in the development of high-performance domain-specific languages that trade off generality to gain both performance and productivity - also applies here. Languages augmented with domain-specific, consistency-aware solvers would support the rapid implementation of formally verified programming abstractions that guarantee distributed consistency. In the long run, we aim to democratize the development of such domain-specific solvers by creating a framework for domain-specific solver development that brings new theory solver implementation within the reach of programmers who are not necessarily SMT solver internals experts.
Cite as

Lindsey Kuper and Peter Alvaro. Toward Domain-Specific Solvers for Distributed Consistency. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuper_et_al:LIPIcs.SNAPL.2019.10,
  author =	{Kuper, Lindsey and Alvaro, Peter},
  title =	{{Toward Domain-Specific Solvers for Distributed Consistency}},
  booktitle =	{3rd Summit on Advances in Programming Languages (SNAPL 2019)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-113-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{136},
  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.2019.10},
  URN =		{urn:nbn:de:0030-drops-105530},
  doi =		{10.4230/LIPIcs.SNAPL.2019.10},
  annote =	{Keywords: distributed consistency, SMT solving, theory solvers}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2017
LIPIcs, Volume 71, SNAPL'17, Complete Volume

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

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

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
DOI: 10.4230/LIPIcs.SNAPL.2017.0
Front Matter, Table of Contents, Preface

Authors: Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi

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

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
DOI: 10.4230/LIPIcs.SNAPL.2017.2
Domain-Specific Symbolic Compilation

Authors: Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, and Nathaniel Yazdani

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

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
Complete Volume
DOI: 10.4230/LIPIcs.SNAPL.2015
LIPIcs, Volume 32, SNAPL'15, Complete Volume

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

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

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

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}
}
  • Refine by Type
  • 14 Document/PDF
  • 6 Document/HTML
  • 2 Volume

  • Refine by Publication Year
  • 1 2026
  • 5 2025
  • 4 2019
  • 4 2017
  • 1 2015
  • Show More...

  • Refine by Author
  • 6 Bodík, Rastislav
  • 5 Krishnamurthi, Shriram
  • 5 Lerner, Benjamin S.
  • 1 Altenkirch, Thorsten
  • 1 Alvaro, Peter
  • Show More...

  • Refine by Series/Journal
  • 12 LIPIcs
  • 1 OASIcs
  • 1 DagRep

  • Refine by Classification
  • 2 Software and its engineering → General programming languages
  • 2 Software and its engineering → Semantics
  • 1 Computing methodologies → Logic programming and answer set programming
  • 1 Computing methodologies → Logical and relational learning
  • 1 Computing methodologies → Supervised learning
  • Show More...

  • Refine by Keyword
  • 2 Front Matter
  • 2 Preface
  • 2 Programming Languages
  • 2 Table of Contents
  • 1 (Directed) hypergraphs
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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