Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
ICFP 2020 (series) / Online /

Room information: TyDe

VenueOnline
Room nameTyDe
Floor0
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

10:00 - 11:30
Session 1TyDe at TyDe
10:00
30m
Talk
Practical Dependent Type Checking Using Twin Types
TyDe
Víctor López Juan Chalmers University of Technology, Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology
Media Attached
10:30
30m
Talk
Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract)
TyDe
Joris Ceulemans Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel
File Attached
11:00
30m
Talk
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract)
TyDe
Ignacio Tiraboschi None, Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET
12:30 - 14:00
Session 2TyDe at TyDe
12:30
30m
Talk
Graded Modal Dependent Type Theory (Extended Abstract)
TyDe
Benjamin Moon School of Computing, University of Kent, Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK
File Attached
13:00
30m
Talk
Frex: indexing modulo equations with free extensions (Extended Abstract)
TyDe
Guillaume Allais University of St Andrews, Edwin Brady University of St. Andrews, UK, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge
13:30
30m
Talk
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
TyDe
Bruce Collie University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
Pre-print
15:30 - 17:00
Session 3TyDe at TyDe
15:30
30m
Talk
Predictable Macros for Hindley-Milner (Extended Abstract)
TyDe
Langston Barrett Galois, Inc, David Thrane Christiansen Galois, USA, Samuel Gélineau SimSpace
16:00
30m
Talk
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
TyDe
Thomas Reynolds University of Missouri, William Harrison Oak Ridge National Laboratory, Rohit Chadha University of Missouri, Gerard Allwein U.S. Naval Research Laboratory
16:30
30m
Talk
Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
TyDe
Mark Lemay Boston University, Cheng Zhang Boston University, William Blair Boston University
18:00 - 19:30
TyDe SocialTyDe at TyDe

Join the Zoom via Clowdr

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

Room10:003011:003012:003013:003014:003015:003016:003017:003018:003019:0030
TyDe

TyDe

Session 1

TyDe

Session 2

TyDe

Session 3

TyDe

TyDe Social

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
TyDe
TyDe
Practical Dependent Type Checking Using Twin Types
10:00 - 10:30
TyDe
Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended ...
10:30 - 11:00
TyDe
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac ...
11:00 - 11:30
TyDe
Graded Modal Dependent Type Theory (Extended Abstract)
12:30 - 13:00
TyDe
Frex: indexing modulo equations with free extensions (Extended Abstract)
13:00 - 13:30
TyDe
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
13:30 - 14:00
TyDe
Predictable Macros for Hindley-Milner (Extended Abstract)
15:30 - 16:00
TyDe
Strongly Bounded Termination with Applications to Security and Hardware ...
16:00 - 16:30
TyDe
Developing a Dependently Typed Language with Runtime Proof Search (Exte ...
16:30 - 17:00