Write a Blog >>
Events (37 results)

Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types

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

… …

How Can I Academia When My Brain Can't Even? Mental Health in Grad School and Beyond

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 …

Gradual Verification of Recursive Heap Data Structures

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

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

Blame tracking at higher fidelity

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 …

Hermes: Implementing Cryptography without Side-channels

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 …

Reasoning about Progress of Concurrent Objects

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

Frex: Free extensions for normalisation by evaluation (invited talk)

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

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

Three equivalent ordinal notation systems in Cubical Agda

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 …

Exorcising Spectres with Secure Compilers

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 …

Trace-Relating Compiler Correctness and Secure Compilation

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 …

Proof Pearl: Braun Trees

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 …

Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq

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 …

Competitive Programming with PiCat

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 …

Undecidability of Higher-Order Unification Formalised in Coq

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 …

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction

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 …

Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages

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 …

A Verified Packrat Parser Interpreter for Parsing Expression Grammars

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

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

Verifying x86 Instruction Implementations

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 …

Invited talk: Matching Logic: The Foundation of the K Framework

CPP 2020 When: Mon 20 Jan 2020 09:00 - 10:00 People: Grigore Rosu, 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 …

The High-Level Benefits of Low-Level Sandboxing

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 …

Internal Type-Theoretic Complexity Analysis

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 …

Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs

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 …

Mechanization of Data Race Freedom guarantee proofs for Weakestmo memory model

Student Research Competition People: Ilya Kaysin

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

A Probabilistic Separation Logic

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 …

Reentrancy? Yes. Reentrancy bug? No.

Student Research Competition People: Zhongye Wang

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

Fast, Sound, and Effectively Complete Dynamic Race Prediction

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 …

What is a Secure Programming Language?

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

Synthesis from Partial Refinement Types

Student Research Competition People: Michael James

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

Full Abstraction for the Quantum Lambda-Calculus

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 …

Actris: Session-Type Based Reasoning in Separation Logic

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 …

Abstract Interpretation of Distributed Network Control Planes

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 …

The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space

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 …

Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation

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. …

Augmented Example-based Synthesis using Relational Perturbation Properties

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. …

Stacked Borrows: An Aliasing Model for Rust

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 …

Optimal Approximate Sampling From Discrete Probability Distributions

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

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

Does Blame Shifting Work?

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

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