ICFP 2020 (series) / TyDe 2020 (series) / TyDe 2020 /
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
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
Sun 23 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
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 |