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