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

Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly-bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed lambda-calculus called the bounded-time lambda-calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.

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

15:30 - 17:00: Session 3TyDe at TyDe
15:30 - 16:00
Predictable Macros for Hindley-Milner (Extended Abstract)
16:00 - 16:30
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas ReynoldsUniversity of Missouri, William HarrisonOak Ridge National Laboratory, Rohit ChadhaUniversity of Missouri, Gerard AllweinU.S. Naval Research Laboratory
16:30 - 17:00
Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
Mark LemayBoston University, Cheng ZhangBoston University, William BlairBoston University