Erlang, a dynamically typed programming language often used in distributed systems, has \textit{success types}. Success types aim to have a dual assertion to the one made in most type systems: that if a program is ill-typed, then the program will not evaluate. Dialyzer, a static analysis tool widely used in practice, implements these types, but a theoretical basis has not yet been created for them. This project focuses on rigorously specifying the type system and creating a proof of correctness for it.
We first build precise definitions of ill-typed and non-evaluating terms on top of existing definitions. Due to “non-evaluating” having a different meaning for ill-typed abstractions, doing so requires a doubly-step-indexed logical relation, the novel contribution of this work. We then use these definitions in a proof by induction to prove reverse type safety.
Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change
18:00 - 20:00 | |||
18:00 2hPoster | Efficient Strong Simulation of High-level Quantum Gates Student Research Competition | ||
18:00 2hPoster | Value semantics in reference-based languages Student Research Competition Hamza Remmal EPFL, LAMP | ||
18:00 2hPoster | Intermittent Concurrency Student Research Competition Myra Dotzel Carnegie Mellon University, Milijana Surbatovich University of Maryland, Limin Jia Carnegie Mellon University | ||
18:00 2hPoster | APIdemic: Verifying Idempotency of REST API Clients Student Research Competition Bhavik Kamlesh Goplani University of Kansas | ||
18:00 2hPoster | Formalizing Erlang’s Success Typings Student Research Competition Elan Semenova University of Maryland, College Park, Leonidas Lampropoulos University of Maryland, College Park | ||
18:00 2hPoster | A Complete Translation from Planning Problems to linear logic Student Research Competition | ||
18:00 2hPoster | Wanco: WebAssembly AOT Compiler that supports Live Migration Student Research Competition | ||
18:00 2hPoster | Increasing the Expressiveness of a Gradual Verifier Student Research Competition Priyam Gupta Purdue University | ||
18:00 2hPoster | M3: A Multi-Stage ML with Mutation Student Research Competition Maite Kramarz University of Toronto | ||
18:00 2hPoster | Loop Invariants Using Neural Networks Student Research Competition Atticus Kuhn University of Cambridge, Abhinandan Pal University of Birmingham, Mirco Giacobbe University of Birmingham | ||
18:00 2hPoster | Property Testing Trace Languages Student Research Competition Jed Koh Jin Keat National University of Singapore | ||
18:00 2hPoster | Optimizing Asynchronous Rust with Hydroflow Student Research Competition Ryan Alameddine University of California, Berkeley | ||
18:00 2hPoster | Relational Hoare Logic for Sequential Program Verification Student Research Competition Shushu Wu Shanghai Jiao Tong University | ||
18:00 2hPoster | Expanding the Scope of Grammar-Based Enumerative Testing Student Research Competition Thea Kjeldsmark University of California, Irvine | ||
18:00 2hPoster | System $F^\omega$ with Coherent Implicit Resolution Student Research Competition Eugene Flesselle EPFL | ||
18:00 2hPoster | The Store-Order Consistency Testing Problem for C-like Memory Models Student Research Competition Grace Tan National University of Singapore | ||
18:00 2hPoster | Formalizing Representation Transformations: A Case Study of Bit Vector Types Student Research Competition Katherine Philip Portland State University | ||