Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Events (37 results)

Reception supported by Facebook

Research Papers When: Thu 17 Jan 2019 18:15 - 19:15

All attendees are welcome! …

Student Research Competition and Reception supported by Microsoft Research

Student Research Competition When: Wed 16 Jan 2019 18:30 - 19:30

All attendees are welcome! …

Research Skills: How to Choose Research Areas

PLMW@POPL When: Tue 15 Jan 2019 11:00 - 11:30 People: Catuscia Palamidessi

… Some of my colleagues stay in the same research area all their life. Others, like me, have changed area many times. In this talk I will explain the motivations that determined my choices, and I will discuss advantages and disadvantages …

Verified Equational Reasoning on a Little Language of Measures

LAFI (né PPS) When: Tue 15 Jan 2019 17:00 - 17:30 People: Matthew Heimerdinger, Chung-chieh Shan

… that all functions are measurable and all measures are s-finite. Combined …

Research Skills: How to Give a Talk

PLMW@POPL When: Tue 15 Jan 2019 10:00 - 10:30 People: Chung-chieh Shan

… in the present. Above all, a talk is an episode of cooperation with other people! So …

A Nuts-and-Bolts Differential Geometric Perspective on Automatic Differentiation

LAFI (né PPS) When: Tue 15 Jan 2019 14:00 - 14:30 People: Barak A. Pearlmutter

… practice of just lifting all reals to duals, focusing on how they differ …

A Simpler Lambda Calculus

PEPM 2019 When: Mon 14 Jan 2019 12:00 - 12:30 People: Barry Jay

… Closure calculus is simpler than pure lambda-calculus as it does not mention free variables or index manipulation, variable renaming, implicit substitution, or any other meta-theory. Further, all programs, even recursive ones, can …

Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs

CoqPL When: Sat 19 Jan 2019 16:00 - 16:25 People: Qinxiang Cao

… Software Toolchain (VST), Iris-rust, Charge! etc. all choose shallow embedding …

Strongly Typed Tracing of Probabilistic Programs (cancelled, alas)

LAFI (né PPS) People: Adam Ścibior, Michael Thomas

… A commonly encountered concept in probabilistic programming literature is that of a trace, which is a record of all the random variables sampled during the program execution. Traces serve two roles, namely providing observed values …

Confidentiality-Preserving Refinement

PriSC 2019 When: Sun 13 Jan 2019 17:00 - 17:30 People: Roberto Guanciale, Christoph Baumann, Mads Dam, Hamed Nemati

… knowledge: if the progression of observer knowledge on all refined computations …

A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra

CPP 2019 When: Tue 15 Jan 2019 14:30 - 15:00 People: Véronique Benzaken, Evelyne Contejean

… a bag semantics hence recovering all well-known algebraic equivalences upon …

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines

CPP 2019 When: Mon 14 Jan 2019 10:00 - 10:30 People: Yannick Forster, Dominique Larchey-Wendling

… phase semantics. We exploit the computability of all functions definable …

A Verified Protocol Buffer Compiler

CPP 2019 When: Tue 15 Jan 2019 14:00 - 14:30 People: Qianchuan Ye, Benjamin Delaware

… and for all the correctness of every generated serializer and deserializer. One …

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

VMCAI 2019 When: Tue 15 Jan 2019 11:00 - 11:30 People: Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis

… input HBD, all possible terms that can be generated by the algorithm … (a question left open in previous work). All results are formalized and proved …

Semantics for Compiler IRs: Undefined Behavior is not Evil!

VMCAI 2019 When: Tue 15 Jan 2019 09:00 - 10:30 People: Nuno P. Lopes

… Building a compiler IR is tricky. First, it should be efficient to compile the desired source language to this IR. Second, the IR should support all the desired optimizations and analyses, and these should run efficiently. Finally …

Termination of Nondeterministic Probabilistic Programs

VMCAI 2019 When: Mon 14 Jan 2019 14:30 - 15:00 People: Hongfei Fu, Krishnendu Chatterjee

… We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show …

Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics

VMCAI 2019 When: Mon 14 Jan 2019 15:00 - 15:30 People: Stefan Haar, Juraj Kolčák, Loïc Paulevé

… of dynamics is lifted to parametric networks, and is proven to preserve all

Relatively Complete Pushdown Analysis of Escape Continuations

VMCAI 2019 When: Sun 13 Jan 2019 17:00 - 17:30 People: Kimball Germane, Matthew Might

… Escape continuations are weaker than full, first-class continuations but nevertheless can express many common control operators. Although language and compiler designs profitably leverage escape continuations, all previous approaches …

Designing Self-Certifying Software Systems

VMCAI 2019 When: Mon 14 Jan 2019 09:00 - 10:30 People: Kedar Namjoshi

… Large software systems are hard to understand. The size and complexity of the implementation, possibly written in a mix of programming languages; a large number of potential configurations; concurrency and distribution, all contribute …

Fully Abstract Module Compilation

Research Papers When: Thu 17 Jan 2019 09:44 - 10:06 People: Karl Crary

… is fully abstract. Consequently, the translation preserves all abstraction present … extension of the underlying core language. All of our proofs are formalized in Coq. …

A Separation Logic for Concurrent Randomized Programs

Research Papers When: Wed 16 Jan 2019 10:57 - 11:19 People: Joseph Tassarotti, Robert Harper

… concurrent skip list. All of our results have been mechanized in Coq. …

Gradual Parametricity, Revisited

Research Papers When: Thu 17 Jan 2019 11:20 - 11:42 People: Matías Toro, Elizabeth Labrada, Éric Tanter

… . In addition to avoiding the uncovered semantic issues, GSF satisfies all …: the dynamic gradual guarantee, which was left as conjecture in all prior work …

An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code

Research Papers When: Fri 18 Jan 2019 16:59 - 17:21 People: Yuting Wang, Pierre Wilke, Zhong Shao

… uniformly for all of its languages and their verified compilation. However, CompCert’s …-grained permissions to stack memory. Using this enriched memory model for all … compilation chain of CompCert, including all the optimization passes. In the end, we …

Iron: Managing Obligations in Higher-Order Concurrent Separation Logic

Research Papers When: Thu 17 Jan 2019 10:36 - 10:58 People: Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal

… . We have formalized all of the developments in the Coq proof assistant. …

Constructing Quotient Inductive-Inductive Types

Research Papers When: Fri 18 Jan 2019 10:57 - 11:19 People: Thorsten Altenkirch, Ambrus Kaposi, András Kovács

… as well. Then, using this syntax we show that all specified QIITs exist …

Adventures in Monitorability: From Branching to Linear Time and Back Again

Research Papers When: Fri 18 Jan 2019 14:29 - 14:51 People: Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingolfsdottir, Karoliina Lehtinen

… fragment is shown to be complete, in the sense that it can express all properties …

Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations

Research Papers When: Fri 18 Jan 2019 13:45 - 14:07 People: Taolue Chen, Matthew Hague, Anthony Widjaja Lin, Philipp Ruemmer, Zhilin Wu

… , replace-all functions (where the replacement string could contain variables …, and acyclic logics), and most existing benchmarks (e.g. most of Kaluza’s, and all … of nondeterministic functions, and operations like one-way transducers, replace-all

Type-Driven Gradual Security with References

Research Papers When: Thu 17 Jan 2019 10:36 - 10:58 People: Matías Toro, Ronald Garcia, Éric Tanter

… noninterference in all programs, even those that enforce security dynamically. We prove that GSLRef satis es all but one of Siek et al.’s criteria for gradually …

Fast and exact analysis for LRU caches

Research Papers When: Fri 18 Jan 2019 17:21 - 17:43 People: Valentin Touzeau, Claire Maiza, David Monniaux, Jan Reineke

… exact classification of all memory accesses as the model-checking approach …

Mechanized Metatheory - The Next Chapter

Research Papers When: Fri 18 Jan 2019 09:05 - 10:05 People: Brigitte Pientka

… of programming languages researchers.

One might be tempted to assume that all is well …

Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs

Research Papers When: Wed 16 Jan 2019 11:19 - 11:41 People: Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, Ranjit Jhala

… equivalent program where all sends, receives, and message bu ers, have been replaced …

Abstraction-Safe Effect Handlers via Tunneling

Research Papers When: Thu 17 Jan 2019 09:00 - 09:22 People: Yizhou Zhang, Andrew Myers

… it is aware of. In our approach, the type system guarantees all effects …

Type-Guided Worst-Case Input Generation

Research Papers When: Thu 17 Jan 2019 15:21 - 15:43 People: Di Wang, Jan Hoffmann

… theorem states that the generated value exhibits the highest cost among all

Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries

Research Papers When: Fri 18 Jan 2019 16:37 - 16:59 People: Xin Yi, Liqian Chen, Xiaoguang Mao, Tao Ji

… approach can efficiently repair (with $100%$ accuracy over all randomly sampled …

Efficient Parameterized Algorithms for Data Packing

Research Papers When: Fri 18 Jan 2019 16:59 - 17:21 People: Krishnendu Chatterjee, Amir Kafshdar Goharshady, Nastaran Okati, Andreas Pavlogiannis

… , all existing techniques for Data Packing are based on heuristics and lack …

Concerto: A Framework for Combined Concrete and Abstract Interpretation

Research Papers When: Fri 18 Jan 2019 10:57 - 11:19 People: John Toman, Dan Grossman

… layers of abstraction, all of which confound even state-of-the-art abstract …

Refinement of Path Expressions for Static Analysis

Research Papers When: Fri 18 Jan 2019 11:41 - 12:03 People: John Cyphert, Jason Breck, Zachary Kincaid, Thomas Reps

… Algebraic program analyses compute information about a program’s behavior by first (a) computing a valid path expression—i.e., a regular expression that recognizes all feasible execution paths (and usually more)—and then (b …