PADL 2020 When: Tue 21 Jan 2020 15:30 - 16:00 People: Philip Wadler

… …

PLMW 2020 When: Tue 21 Jan 2020 15:40 - 16:40 People: Kenny Foner

… , but I also want all listeners to be empowered to choose (either before or at any …

WGT When: Sat 25 Jan 2020 15:35 - 16:07 People: Jenna Wise (DiVincenzo), Johannes Bader, Jonathan Aldrich, Éric Tanter, Joshua Sunshine

… , if at all. It draws from research on gradual typing to produce a verification system …

WGT When: Sat 25 Jan 2020 16:50 - 17:20 People: Jakub Zalewski, James McKinna, J. Garrett Morris, Philip Wadler

… This paper introduces λdB, a blame calculus with dependent types. It supports dependent functions, predicate refinement at all types, the dynamic type, and full blame tracking. It is inspired by and extends previous work on hybrid types …

Principles of Secure Compilation 2020 When: Sat 25 Jan 2020 11:42 - 12:06 People: Ken Friis Larsen, Torben Mogensen, Michael Kirkedal Thomsen

… ensures that all variables are cleared after use, thus avoiding state information …

PEPM 2020 When: Mon 20 Jan 2020 14:00 - 15:00 People: Xinyu Feng

… together for concurrent objects. It unifies thread-modular reasoning about all …

PEPM 2020 When: Mon 20 Jan 2020 15:35 - 16:10 People: Ohad Kammar

… amounts to a universal property, by ranging all possible algebra …

CPP 2020 When: Mon 20 Jan 2020 17:12 - 17:34 People: Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani

… they admit a transfinite induction principle. We prove that all three … using the univalence principle. All our constructions have been implemented …

Principles of Secure Compilation 2020 When: Sat 25 Jan 2020 10:30 - 10:54 People: Marco Patrignani, Marco Guarnieri

… Speculative execution attacks like Spectre can be used to violate confidentiality in all modern general-purpose CPUs. Recently, many compiler-level countermeasures have been proposed to mitigate the impact of Spectre-style attacks. However …

Principles of Secure Compilation 2020 When: Sat 25 Jan 2020 10:54 - 11:18 People: Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Éric Tanter, Jérémy Thibault

… Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here …

CPP 2020 When: Mon 20 Jan 2020 10:51 - 11:13 People: Tobias Nipkow, Thomas Sewell

… the missing proofs and verify all of these algorithms in Isabelle, including …

CPP 2020 When: Tue 21 Jan 2020 16:18 - 16:40 People: Christian Doczkal, Damien Pous

… representation employing a fixed type of vertices shared among all graphs …

PADL 2020 When: Mon 20 Jan 2020 16:20 - 17:00 People: Neng-Fa Zhou

… .^[1] The problems are all combinatorial, and all have practical …

CPP 2020 When: Mon 20 Jan 2020 16:18 - 16:40 People: Simon Spies, Yannick Forster

… for first-order unification.

All proofs are carried out in the setting …

CPP 2020 When: Tue 21 Jan 2020 14:43 - 15:05 People: Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser

… that all values are used linearly, and that linearity is maintained throughout …

CPP 2020 When: Mon 20 Jan 2020 14:00 - 14:21 People: Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic

… .

All of the results in this paper have been proved in Coq …

CPP 2020 When: Mon 20 Jan 2020 11:45 - 12:07 People: Shilpi Goel, Anna Slobodova, Rob Sumners, Sol Swords

… -operations in execution units. All these tasks are performed within one …

CPP 2020 When: Mon 20 Jan 2020 09:00 - 10:00 People: Grigore Roşu, Xiaohong Chen

… The K framework (kframework.org) is an effort in realizing the ideal language framework, where programming languages must have formal semantics and all language tools are automatically generated from the formal semantics. Until recently …

CPP 2020 When: Mon 20 Jan 2020 10:30 - 10:51 People: Clément Blaudeau, Natarajan Shankar

… to the reference one. All of the parsers are executable. The proofs are formalized …

Research Papers When: Fri 24 Jan 2020 10:51 - 11:13 People: Michael Sammler, Deepak Garg, Derek Dreyer, Tadeusz Litak

… ) are upheld in the presence of arbitrary untrusted code, so long as all interactions with untrusted code occur at the “any” type (a type inhabited by all values … between the “any” type and much richer types. All results of this paper …

Student Research Competition People: Roland Samuelson

… ability to reason about all programs expressible in the calculus of constructions …. Finally, we prove a faithfulness property, showing that all internally computed …

Student Research Competition People: Ilya Kaysin

… weaker than SC (or any data races) in his/her code is enough to rule out all …

Research Papers When: Fri 24 Jan 2020 12:07 - 12:30 People: Federico Aschieri, Francesco A. Genco

… shall prove that λ_{par} satisfies all the desirable properties for a typed …

Research Papers When: Fri 24 Jan 2020 14:43 - 15:05 People: Gilles Barthe, Justin Hsu, Kevin Liao

… —a basic operation in all probabilistic languages—and greatly simplifies formal … methods handle independence poorly, if at all.

In this paper, we propose …

Student Research Competition People: Zhongye Wang

… language to demonstrate our results and formalize all definitions and proofs in Coq. …

Research Papers When: Thu 23 Jan 2020 09:00 - 10:00 People: Cristina Cifuentes

… will come more security. But we contend that all of today’s mainstream programming … account for over 50% of all reported software vulnerabilities … at least one of these categories, interestingly, we find that none address all …

Research Papers When: Thu 23 Jan 2020 11:45 - 12:07 People: Andreas Pavlogiannis

… is to determine all pairs of events of t that constitute a data race … processes, i.e., it provably detects all races in the trace. We also develop … that it has detected all races in the benchmark set, hence the reports are both …

Student Research Competition People: Michael B. James

… specify what the program must do on all valid inputs. However, writing …

Research Papers When: Thu 23 Jan 2020 14:21 - 14:43 People: Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker

… for all destinations for 95% of the networks and for most destinations …

Research Papers When: Fri 24 Jan 2020 14:00 - 14:21 People: Pierre Clairambault, Marc De Visme

… by summing valuations of all states matching a given observable. Our proof method …

Research Papers When: Wed 22 Jan 2020 14:43 - 15:05 People: Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers

… execution of programs, as well as all examples in the paper, in the Coq proof …

Research Papers When: Wed 22 Jan 2020 10:30 - 10:51 People: Yannick Forster, Fabian Kunze, Marc Roth

… a polynomial overhead in time and a constant factor overhead in space for all …; in particular, all substitutions are executed immediately. This simulation runs …

Research Papers When: Thu 23 Jan 2020 10:51 - 11:13 People: Shengwei An, Rishabh Singh, Sasa Misailovic, Roopsha Samanta

… of Sketch for all three user interfaces. …

Research Papers When: Wed 22 Jan 2020 14:43 - 15:05 People: Lukas Lazarek, Alexis King, Samanvitha Sundar, Robert Bruce Findler, Christos Dimoulas

… to the faulty component in all cases; and (ii) Racket contracts interfere …

Research Papers When: Fri 24 Jan 2020 10:30 - 10:51 People: Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon

… correctness guarantee. All the proofs are implemented in the Coq proof assistant. …

Research Papers When: Thu 23 Jan 2020 16:18 - 16:40 People: Feras Saad, Cameron Freer, Martin C. Rinard, Vikash K. Mansinghka

… all entropy-optimal sampling algorithms that operate within the specified …

Research Papers When: Fri 24 Jan 2020 14:00 - 14:21 People: Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer

… the semantics of their code despite all the optimizations it is doing …