Events (62 results)

The Curse of Knowledge

PLMW When: Tue 9 Jan 2018 14:30 - 15:00 People: Benjamin C. Pierce

… Writing well is hard for many reasons, but perhaps the hardest of all is what Steven Pinker calls “The Curse of Knowledge” — the difficulty of imagining ourselves inside the mind of someone who does not know something that we do know …

Lightning Overview - Day 3

Research Papers When: Fri 12 Jan 2018 09:30 - 10:00

… 1-minute overview of all the talks on Day 3. …

Lightning Overview - Day 1

Research Papers When: Wed 10 Jan 2018 09:45 - 10:05

… 1-minute overview of all the talks on Day 1. …

Lightning Overview - Day 2

Research Papers When: Thu 11 Jan 2018 09:30 - 10:00

… 1-minute overview of all the talks on Day 2. …

SweetPea: A Language for Designing Experiments

Off the Beaten Track 2018 When: Sat 13 Jan 2018 14:00 - 14:30 People: Annie Cherkaev, Sebastian Musslick, Jonathan Cohen, Vivek Srikumar, Matthew Flatt

… of all valid solutions. …

Explaining Type Errors

Off the Beaten Track 2018 When: Sat 13 Jan 2018 11:30 - 12:00 People: Brent Yorgey, Richard A. Eisenberg, Harley D. Eades III

… ", but ought to have all the tools of programming language theory and practice …

INVITED TALK: ``Safe'' Languages Require Sequential Consistency

PADL 2018 When: Mon 8 Jan 2018 14:00 - 14:30 People: Todd Millstein

… Almost all languages today are memory safe, thereby providing simple and strong guarantees to all programs. Yet the concurrency semantics of these “safe” languages causes similar problems as arise in memory-unsafe languages: small program …

A Coq Formalisation of a Core of R

When: Sat 13 Jan 2018 14:25 - 14:50 People: Martin Bodin

… Real-world programming languages have subtle behaviours. In particular, their semantics is often associated with various corner cases. Programmers are sometimes unaware of all these corner cases, which can yield to serious bugs …

Hygienic Source-Code Generation Using Functors

PADL 2018 When: Tue 9 Jan 2018 10:30 - 11:00 People: Karl Crary

… that are then instantiated by the programmer with appropriate action code. This results in all code …

Building Secure SGX Enclaves using F*, C/C++ and X64

PriSC 2018 When: Sat 13 Jan 2018 13:30 - 14:00 People: Anitha Gollamudi, Cédric Fournet

… to standalone C code. However, this does not account for all code running within … and for core libraries. Besides, we cannot expect all enclave applications …

Gradually Typed Symbolic Expressions

PEPM 2018 When: Mon 8 Jan 2018 14:30 - 15:00 People: David Broman, Jeremy G. Siek

… , statically typed, and dynamically typed variants, all having their pros and cons …-specific modeling languages, all within the domain of physical modeling …

Recursive Programs in Normal Form (Short Paper)

PEPM 2018 When: Tue 9 Jan 2018 15:00 - 15:30 People: Barry Jay

… that support queries of internal program structure. In all these settings, partial …

Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)

PEPM 2018 When: Tue 9 Jan 2018 16:40 - 16:50 People: Cyprien Mangin, Matthieu Sozeau

… of all, we describe the splitting tree, the intermediate data structure used …

Short talk: Dependently Typed Assembly for Secure Linking

PriSC 2018 When: Sat 13 Jan 2018 11:35 - 11:40 People: William J. Bowman

… cannot express all security invariants we wish to enforce. Dependent types could …

Robust Hyperproperty Preservation for Secure Compilation

PriSC 2018 When: Sat 13 Jan 2018 14:00 - 14:30 People: Deepak Garg, Cătălin Hriţcu, Marco Patrignani, Marco Stronati, David Swasey

… preservation of all hyperproperties, seems achievable for simple transformations …

Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs

PriSC 2018 When: Sat 13 Jan 2018 16:30 - 17:00 People: Robert Sison

… Domain Desktop Compositor, and instantiated all of the related proofs of security …

Formally Secure Compilation of Unsafe Low-Level Components

PriSC 2018 When: Sat 13 Jan 2018 14:30 - 15:00 People: Guglielmo Fachini, Cătălin Hriţcu, Marco Stronati, Ana Nora Evans, Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach

… . Each component is protected from all the others until it receives an input …

Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)

PriSC 2018 When: Sat 13 Jan 2018 09:10 - 10:00 People: Mathias Payer

… into a derived class. A type sanitizer tracks the types of all objects and makes …

Generic Derivation of Induction for Impredicative Encodings in Cedille

CPP 2018 When: Tue 9 Jan 2018 14:00 - 14:30 People: Denis Firsov, Aaron Stump

… products,
primitive heterogeneous equality, and dependent intersections.
All

Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq

CPP 2018 When: Mon 8 Jan 2018 11:30 - 12:00 People: Christian Doczkal, Joachim Bard

… without converse and then extend the proofs to Converse PDL. All results …

Formal Methods For Probabilistic Programming

PPS 2018 When: Tue 9 Jan 2018 11:30 - 12:00 People: Daniel Selsam

… correctly on all inputs using tools from software verification and formal mathematics. …

More support for symbolic disintegration

PPS 2018 When: Tue 9 Jan 2018 15:00 - 15:30 People: Praveen Narayanan, Chung-chieh Shan

… . The conditioning tool applies uniform reasoning across all three kinds of applications. …

Mechanising and Verifying the WebAssembly Specification

CPP 2018 When: Mon 8 Jan 2018 13:30 - 14:00 People: Conrad Watt

… <p>WebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js …

Binder Aware Recursion over Well-Scoped de Bruijn Syntax

CPP 2018 When: Tue 9 Jan 2018 17:30 - 18:00 People: Jonas Kaiser, Steven Schäfer, Kathrin Stark

… foundation of future versions of the Autosubst Coq library. All developments …

Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)

CPP 2018 When: Mon 8 Jan 2018 09:00 - 10:00 People: Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann, Akihisa Yamada


involves the computation of all eigenvalues of $A$, which
often leads to expensive …

Mechanising Blockchain Consensus

CPP 2018 When: Mon 8 Jan 2018 14:30 - 15:00 People: George Pîrlea, Ilya Sergey

… consensus, and discuss their adequacy.

All results described in this paper …

Proofs in Conflict-Driven Theory Combination

CPP 2018 When: Tue 9 Jan 2018 11:30 - 12:00 People: Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

… : it assumes that all theory modules produce proof objects and it accommodates …

Triangulating Context Lemmas

CPP 2018 When: Mon 8 Jan 2018 16:00 - 16:30 People: Craig McLaughlin, James McKinna, Ian Stark

… to a CIU result formulated with frame stacks.

All this is formalised and proved …

Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts

Artifact Evaluation People: Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

… . By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contracts, excluding the DAO or contracts …

Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts

Research Papers When: Fri 12 Jan 2018 11:45 - 12:10 People: Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar

… and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contracts, excluding …

Migrating Gradual Types

Research Papers When: Wed 10 Jan 2018 14:30 - 14:55 People: John Peter Campora, Sheng Chen, Martin Erwig, Eric Walkingshaw

… as possible, in general, all possible combinations of adding or removing type annotations … this problem by developing migrational typing, which efficiently types all

Migrating Gradual Types

Artifact Evaluation People: John Peter Campora, Sheng Chen, Martin Erwig, Eric Walkingshaw

… , in general, all possible combinations of adding or removing type annotations from … this problem by developing \emph{migrational typing}, which efficiently types all possible …

A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST

Artifact Evaluation People: Amin Timany, Leo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal

… formalized all the technical development and results in Coq. …

A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST

Research Papers When: Fri 12 Jan 2018 15:50 - 16:15 People: Amin Timany, Leo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal

… formalized all the technical development and results in Coq. …

Soft Contract Verification for Higher-order Stateful Programs

Artifact Evaluation People: Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

… discovery. So contract verification aims to guarantee all or most … functions, modularity, and statefulness. Our approach tackles all these features … 99.94% of checks statically (all but 28 of 51,713).

Stateful, higher-order …

Soft Contract Verification for Higher-order Stateful Programs

Research Papers When: Fri 12 Jan 2018 11:20 - 11:45 People: Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn

… discovery. So contract verification aims to guarantee all or most … functions, modularity, and statefulness. Our approach tackles all these features … 99.94% of checks statically (all but 28 of 51, 713).

Stateful, higher-order …

A new proof rule for almost-sure termination

Research Papers When: Thu 11 Jan 2018 13:40 - 14:05 People: Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen

… We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its …

Symbolic Types for Lenient Symbolic Execution

Research Papers When: Thu 11 Jan 2018 14:55 - 15:20 People: Stephen Chang, Alex Knauth, Emina Torlak

… We present \lcsym, a typed $\lambda$-calculus for lenient symbolic execution, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our …

Symbolic Types for Lenient Symbolic Execution

Artifact Evaluation People: Stephen Chang, Alex Knauth, Emina Torlak

… We present \lcsym, a typed $\lambda$-calculus for \emph{lenient symbolic execution}, where some language constructs do not recognize symbolic values. Its type system, however, ensures safe behavior of all symbolic values in a program. Our …

Simplicitly: Foundations and Applications of Implicit Function Types

Artifact Evaluation People: Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki

… Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts …

Simplicitly: Foundations and Applications of Implicit Function Types

Research Papers When: Thu 11 Jan 2018 16:15 - 16:40 People: Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki

… Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define …

String Constraints with Concatenation and Transducers Solved Efficiently

Research Papers When: Wed 10 Jan 2018 11:45 - 12:10 People: Lukas Holik, Anthony Widjaja Lin, Petr Janku, Philipp Ruemmer, Tomas Vojnar

… the importance of incorporating the replace-all operator (i.e. replace all

String Constraints with Concatenation and Transducers Solved Efficiently

Artifact Evaluation People: Lukas Holik, Petr Janku, Anthony Widjaja Lin, Philipp Ruemmer, Tomas Vojnar

… the importance of incorporating the replace-all operator (i.e. replace all

Programming and Proving with Distributed Protocols

Research Papers When: Thu 11 Jan 2018 11:45 - 12:10 People: Ilya Sergey, James R. Wilcox, Zachary Tatlock

… commit), so all their internal invariants hold, and (b) correctly composing … verification of distributed systems and their clients, all within the mechanized …

Programming and Proving with Distributed Protocols

Artifact Evaluation People: Ilya Sergey, James R. Wilcox, Zachary Tatlock

… commit), so all their internal invariants hold, and (b) correctly composing … verification of distributed systems and their clients, all within the mechanized …

Code Obfuscation - A Hacking view on program analysis and understanding.

TutorialFest When: Mon 8 Jan 2018 09:00 - 10:30Mon 8 Jan 2018 11:00 - 12:00 People: Roberto Giacobazzi

… these attacks. Attacks are inhibited by maximising imprecision in all attempts made …

Introduction to Algebraic Program analysis.

TutorialFest When: Mon 8 Jan 2018 16:00 - 17:00Mon 8 Jan 2018 14:00 - 15:30 People: Zachary Kincaid, Thomas Reps

… converging upon a property that over-approximates all of the reachable states …

What's Decidable About String Constraints with ReplaceAll Function?

Research Papers When: Wed 10 Jan 2018 11:20 - 11:45 People: Taolue Chen, Yan Chen, Matthew Hague, Anthony Widjaja Lin, Zhilin Wu

… either the first occurrence or all occurrences of a ``pattern'' string constant … of the string-replace function (especially the replace-all facility) is increasingly …

WebRelate: Integrating Web Data with Spreadsheets using Examples

Research Papers When: Wed 10 Jan 2018 10:55 - 11:20 People: Jeevana Priya Inala, Rishabh Singh

… generates the URLs for the webpages containing the desired data for all rows …

Optimal Dyck Reachability for Data-dependence and Alias Analysis

Artifact Evaluation People: Krishnendu Chatterjee, Bhavya Choudhary, Andreas Pavlogiannis

… demonstrates that the new algorithms significantly outperform all existing methods …

Optimal Dyck Reachability for Data-dependence and Alias Analysis

Research Papers When: Thu 11 Jan 2018 10:55 - 11:20 People: Krishnendu Chatterjee, Andreas Pavlogiannis, Bhavya Choudhary

… demonstrates that the new algorithms significantly outperform all existing methods …

WebRelate: Integrating Web Data with Spreadsheets using Examples

Artifact Evaluation People: Jeevana Priya Inala, Rishabh Singh

… the URLs for the webpages containing the desired data for all rows …

Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8

Research Papers When: Wed 10 Jan 2018 16:40 - 17:05 People: Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell

… before becoming visible to all — but this has not been exploited in production …

Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8

Artifact Evaluation People: Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell

… becoming visible to all — but this has not been exploited in production …

A Practical Construction for Decomposing Numerical Abstract Domains

Research Papers When: Fri 12 Jan 2018 14:30 - 14:55 People: Gagandeep Singh, Markus Püschel, Martin Vechev

… of abstract domains to benefit from decomposition without re-writing all

A Practical Construction for Decomposing Numerical Abstract Domains

Artifact Evaluation People: Gagandeep Singh, Markus Püschel, Martin Vechev

… domains to benefit from decomposition without re-writing all

Reducing Liveness to Safety in First-Order Logic

Research Papers When: Thu 11 Jan 2018 10:55 - 11:20 People: Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham

… after satisfying all fairness constraints). However, with both infinitely many …

Reducing Liveness to Safety in First-Order Logic

Artifact Evaluation People: Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham

… satisfying all fairness constraints). However, with both infinitely many states …

Collapsing Towers of Interpreters

Artifact Evaluation People: Nada Amin, Tiark Rompf

… Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass …

Collapsing Towers of Interpreters

Research Papers When: Fri 12 Jan 2018 11:45 - 12:10 People: Nada Amin, Tiark Rompf

… Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass …

Parametricity versus the Universal Type

Research Papers When: Thu 11 Jan 2018 14:05 - 14:30 People: Dominique Devriese, Marco Patrignani, Frank Piessens

… '' type, i.e., a type where all other types can be injected to and extracted from …

Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can)

Research Papers When: Wed 10 Jan 2018 08:45 - 09:45 People: Derek Dreyer

… .

Unfortunately, syntactic type soundness is a rather weak theorem. First of all, its …