Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 13:30 - 14:00 at TyDe - Session 2

Symbolic holes are one of the fundamental building blocks of solver-aided and interactive programming. Unknown values can be soundly integrated into programs, and automated tools such as SAT solvers can be used to prove properties of programs containing them. However, supporting symbolic holes in a programming language is challenging; specifying interactions of holes with the type system and execution semantics requires careful design.

This paper motivates and introduces the implementation of untyped symbolic holes to LLVM IR, a strongly-typed compiler intermediate language. We describe how such holes can be implemented safely by abstracting unsound and type-unsafe details behind a new primitive IR manipulation. Our implementation co-operates well with existing features such as type and dependency checking. Finally, we highlight potentially fruitful areas for investigation using our implementation.

Sun 23 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

12:30 - 14:00: Session 2TyDe at TyDe
12:30 - 13:00
Graded Modal Dependent Type Theory (Extended Abstract)
Benjamin MoonSchool of Computing, University of Kent, Harley D. Eades IIIAugusta University, Dominic OrchardUniversity of Kent, UK
File Attached
13:00 - 13:30
Frex: indexing modulo equations with free extensions (Extended Abstract)
Guillaume AllaisUniversity of St Andrews, Edwin BradyUniversity of St. Andrews, UK, Ohad KammarUniversity of Edinburgh, Jeremy YallopUniversity of Cambridge
13:30 - 14:00
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
Bruce CollieUniversity of Edinburgh, Michael F. P. O'BoyleUniversity of Edinburgh