TyDe 2021
Sun 22 - Mon 23 August 2021
co-located with ICFP 2021
ICFP 2021 (series) / TyDe 2021 (series) / Virtual /

Room information: ML

VenueVirtual
Room nameML
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

Thu 26 Aug

Displayed time zone: Seoul change

18:00 - 19:30
Semantics & VerificationML at ML
Chair(s): Martin Elsman University of Copenhagen, Denmark
18:00
30m
Talk
Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming
ML
Daniel Hillerström The University of Edinburgh
Pre-print Media Attached
18:30
30m
Talk
Cameleer: a Deductive Verification Tool for OCaml
ML
Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
File Attached
19:00
30m
Talk
Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques
ML
Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London
File Attached
20:00 - 21:30
Compiler & Language CorrectnessML at ML
Chair(s): Robert Atkey University of Strathclyde
20:00
30m
Talk
Formalizing OCaml GADT typing in Coq
ML
Jacques Garrigue Nagoya University, Xuanrui Qi Nagoya University
Pre-print File Attached
20:30
30m
Talk
Demo Paper : Coqlex, an approach to generate verified lexers
ML
Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique
Media Attached File Attached
21:00
30m
Talk
Code Extraction from Coq to ML-like languages
ML
Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University
Link to publication File Attached
22:00 - 23:30
KeynoteML at ML
22:00
60m
Keynote
Keynote: Narratives and Lessons from The Early History of F#
ML
Don Syme Microsoft
23:30 - 01:00
Language & Library DesignML at ML
Chair(s): Benoît Montagu Inria
23:30
30m
Talk
A metalanguage for multi-phase modularity
ML
Jonathan Sterling Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA
File Attached
00:00
30m
Talk
Unfolding ML datatype declarations without loops
ML
Nicolas Chataing ENS Paris, Gabriel Scherer INRIA Saclay
Pre-print Media Attached
00:30
30m
Talk
Verifying Multiparty Communication Protocols using ML Type Systems
ML
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
File Attached

Fri 27 Aug

Displayed time zone: Seoul change

01:30 - 03:00
Inference + Short talks ML at ML
Chair(s): Ohad Kammar University of Edinburgh
01:30
30m
Talk
Frozen inference constraints for type-directed disambiguation
ML
Olivier Martinot INRIA, Gabriel Scherer INRIA Saclay
Pre-print Media Attached
02:00
15m
Talk
Experience Report: Domain Modeling with F# (short talk)
ML
Scott Wlaschin None
Media Attached File Attached
02:15
15m
Talk
Isomorphisms are back! (short talk)
ML
Clément Allain Inria, Gabriel Radanne Inria, Laure Gonnord University of Lyon & LIP, France
File Attached
02:30
15m
Talk
Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk)
ML
Allister Beharry None
Media Attached File Attached
02:45
15m
Talk
A Data-centered User Study for jsCoq (short talk)
ML
Hanneli Tavante McGill University
File Attached

Thu 26 Aug

Displayed time zone: Seoul change

Room18:003019:003020:003021:003022:003023:00300:0030
ML

ML

Semantics & Verification

ML

Compiler & Language Correctness

ML

Keynote

ML

Language & Library Design

Fri 27 Aug

Displayed time zone: Seoul change

Room1:00302:0030
ML

ML

Inference + Short talks

Thu 26 Aug

Displayed time zone: Seoul change

Room18:0015304519:0015304520:0015304521:0015304522:0015304523:00153045
ML
ML
Composing UNIX with Effect Handlers: A Case Study in Effect Handler Ori ...
18:00 - 18:30
ML
Cameleer: a Deductive Verification Tool for OCaml
18:30 - 19:00
ML
Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation U ...
19:00 - 19:30
ML
Formalizing OCaml GADT typing in Coq
20:00 - 20:30
ML
Demo Paper : Coqlex, an approach to generate verified lexers
20:30 - 21:00
ML
Code Extraction from Coq to ML-like languages
21:00 - 21:30
ML
Keynote: Narratives and Lessons from The Early History of F#
22:00 - 23:00
ML
A metalanguage for multi-phase modularity
23:30 - 00:00

Fri 27 Aug

Displayed time zone: Seoul change

Room0:001530451:001530452:00153045
ML
ML
Unfolding ML datatype declarations without loops
00:00 - 00:30
ML
Verifying Multiparty Communication Protocols using ML Type Systems
00:30 - 01:00
ML
Frozen inference constraints for type-directed disambiguation
01:30 - 02:00
ML
Experience Report: Domain Modeling with F# (short talk)
02:00 - 02:15
ML
Isomorphisms are back! (short talk)
02:15 - 02:30
ML
Sylvester: Unified, typed, notation for symbolic mathematics and proofs ...
02:30 - 02:45
ML
A Data-centered User Study for jsCoq (short talk)
02:45 - 03:00