Wed 17 Jul 2019 13:50 - 14:10 at Mancy - Types Chair(s): Davide Ancona

Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) cores. There are well described interaction protocols for communication between IP Cores. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such a separation of concerns, such tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.

Wed 17 Jul
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:30 - 15:10
TypesResearch Papers at Mancy
Chair(s): Davide AnconaUniversity of Genova
13:30
20m
Research paper
Transient Typechecks are (Almost) Free
Research Papers
Richard RobertsVictoria University of Wellington, Stefan MarrUniversity of Kent, Michael HomerVictoria University of Wellington, James NobleVictoria University of Wellington
DOI Media Attached
13:50
20m
Research paper
A Typing Discipline for Hardware Interfaces
Research Papers
Jan de Muijnck-HughesUniversity of Glasgow, Wim VanderbauwhedeUniversity of Glasgow
DOI Media Attached
14:10
20m
Research paper
Minimal Session TypesPearl
Research Papers
Alen ArslanagićUniversity of Groningen, Jorge A. PérezUniversity of Groningen, The Netherlands, Erik VoogdUniversity of Groningen
DOI Media Attached
14:30
20m
Research paper
Julia's Efficient Algorithm for Subtyping Unions and Covariant TuplesPearl
Research Papers
Benjamin ChungNortheastern University, Francesco Zappa NardelliInria, Jan VitekNortheastern University
DOI Media Attached
14:50
20m
Research paper
On Satisfiability of Nominal Subtyping with Variance
Research Papers
Aleksandr MisonizhnikSaint-Petersburg State University, Dmitry MordvinovSaint-Petersburg State University, JetBrains Research
DOI Media Attached