ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Events (23 results)

Asterisk: Secure Programming Language for Smart Contracts (Student Talk)

Scala When: Wed 18 Nov 2020 11:40 - 12:00 People: Mohammadreza Ashouri

… by Asterisk are cross-platform in the sense that a compiled contract runs on all

Prusti – Deductive Verification for Rust

FTfJP People: Alexander J. Summers

… ; in particular, specifications and all interactions with our implemented tool …

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Research Papers When: Tue 17 Nov 2020 01:20 - 01:40Mon 16 Nov 2020 13:20 - 13:40 People: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner

… async/await APIs, all underpinned by a simple Core Event Semantics that is sufficiently expressive to describe the event models underlying all these APIs. Our … official test-suites, passing all the applicable tests. Using the Core Events …

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Artifacts People: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner

… async/await APIs, all underpinned by a simple Core Event Semantics that is sufficiently expressive to describe the event models underlying all these APIs. Our … official test-suites, passing all the applicable tests. Using the Core Events …

Owicki-Gries Reasoning for C11 RAR

Artifacts People: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

… the formalisation and proof of all case studies presented in the paper. All

Multiparty Session Programming with Global Protocol Combinators

Artifacts People: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen

… . Local behaviours for all processes in a protocol are inferred at once from … of ocaml-mpst, with all the examples and benchmarks discussed in the paper …

K-LLVM: A Relatively Complete Semantics of LLVM IR

Research Papers When: Mon 16 Nov 2020 01:00 - 01:20Sun 15 Nov 2020 13:00 - 13:20 People: Liyi Li, Elsa Gunter

… complete formal LLVM IR semantics to date, including all LLVM IR instructions … an abstract machine that executes all LLVM IR instructions. The machine allows … consistent memory model and does not include all LLVM concurrency memory behaviors …

The Duality of Subtyping (artifact)

Artifacts People: Bruno C. d. S. Oliveira, Shaobo Cui, Baber Rehman

… image with all the dependencies installed or it could be built from the scratch …

Blame for Null

Research Papers When: Sun 15 Nov 2020 21:40 - 22:00Sun 15 Nov 2020 09:40 - 10:00 People: Abel Nieto, Marianna Rapoport, Gregor Richards, Ondřej Lhoták

… Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All … can’t be blamed. All our results are formalized in the Coq proof assistant. …

Static Type Analysis by Abstract Interpretation of Python Programs

Artifacts People: Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

… in the experimental evaluation of the paper (Fig. 13).

All analyzers have been compiled …

Perfect is the Enemy of Good: Best-Effort Program Synthesis

Research Papers When: Sun 15 Nov 2020 22:00 - 22:20Sun 15 Nov 2020 10:00 - 10:20 People: Hila Peleg, Nadia Polikarpova

… always satisfy the specification exactly. We conjecture that this all-or-nothing … then not, no result at all. In this paper we propose a new program synthesis paradigm we call … even when the specification is flawed or too hard: i) for all benchmarks …

Perfect is the Enemy of Good: Best-Effort Program Synthesis

Artifacts People: Hila Peleg, Nadia Polikarpova

… always satisfy the specification exactly. We conjecture that this all-or-nothing … then not, no result at all. In this paper we propose a new program synthesis paradigm we call … when the specification is flawed or too hard: (i) for all benchmarks …

Scala with Explicit Nulls

Research Papers When: Mon 16 Nov 2020 06:00 - 06:20Sun 15 Nov 2020 18:00 - 18:20 People: Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, Justin Pu

… The Scala programming language makes all reference types implicitly nullable. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors. In this paper, we …

Owicki-Gries Reasoning for C11 RAR

Research Papers When: Mon 16 Nov 2020 03:40 - 04:00Sun 15 Nov 2020 15:40 - 16:00 People: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

… with both relaxed and release-acquire accesses) that allows all Owicki-Gries …

Blame for Null

Artifacts People: Abel Nieto, Marianna Rapoport, Ondřej Lhoták, Gregor Richards

… . All of the above also need to interoperate with languages where types remain … \emph{explicitly nullable programs can’t be blamed}. All our results …

Scala with Explicit Nulls

Artifacts People: Abel Nieto, Ondřej Lhoták, Yaoyu Zhao, Angela Chang, Justin Pu

… The Scala programming language makes \emph{all} reference types \emph{implicitly nullable}. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors …

Row and Bounded Polymorphism via Disjoint Polymorphism

Research Papers When: Mon 16 Nov 2020 00:00 - 00:20Sun 15 Nov 2020 12:00 - 12:20 People: Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, Tom Schrijvers

… intersection types* and disjoint polymorphism. With all these alternatives …

Multiparty Session Programming with Global Protocol Combinators

Research Papers When: Mon 16 Nov 2020 05:40 - 06:00Sun 15 Nov 2020 17:40 - 18:00 People: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen

… and verifying multiparty protocols in OCaml. Local behaviours for all processes …

Static Type Analysis by Abstract Interpretation of Python Programs

Research Papers When: Mon 16 Nov 2020 02:00 - 02:20Sun 15 Nov 2020 14:00 - 14:20 People: Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

… precisely track all exceptions (raised or caught). We designed a static analysis …

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Artifacts People: Xuejing Huang, Bruno C. d. S. Oliveira

… with respect to the $\lambda_{i}$ type system. All results have been fully …

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Research Papers When: Mon 16 Nov 2020 01:20 - 01:40Sun 15 Nov 2020 13:20 - 13:40 People: Xuejing Huang, Bruno C. d. S. Oliveira

… }^{:}$ is complete with respect to the $\lambda_{i}$ type system. All results have …

SqueakLive

Tutorials People: Marcel Taeumel, Patrick Rein, Tobias Pape, Tim Felgentreff, Robert Hirschfeld

… , tools, applications) with fast execution environments for all major platforms …

Polyglot Programming

Tutorials People: Fabio Niephaus, Tim Felgentreff, Mario Wolczko, Robert Hirschfeld

… an example notebook, and explain how it works under the hood. Together with all