ML 2021
Sun 22 - Fri 27 August 2021
co-located with ICFP 2021
ICFP 2021 (series) / ML 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 2021 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 2021
Daniel Hillerström The University of Edinburgh
Pre-print Media Attached
18:30
30m
Talk
Cameleer: a Deductive Verification Tool for OCaml
ML 2021
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 2021
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 2021 at ML
Chair(s): Robert Atkey University of Strathclyde
20:00
30m
Talk
Formalizing OCaml GADT typing in Coq
ML 2021
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 2021
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 2021
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 2021 at ML
22:00
60m
Keynote
Keynote: Narratives and Lessons from The Early History of F#
ML 2021
Don Syme Microsoft
23:30 - 01:00
Language & Library DesignML 2021 at ML
Chair(s): Benoît Montagu Inria
23:30
30m
Talk
A metalanguage for multi-phase modularity
ML 2021
Jonathan Sterling Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA
File Attached
00:00
30m
Talk
Unfolding ML datatype declarations without loops
ML 2021
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 2021
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 2021 at ML
Chair(s): Ohad Kammar University of Edinburgh
01:30
30m
Talk
Frozen inference constraints for type-directed disambiguation
ML 2021
Olivier Martinot INRIA, Gabriel Scherer INRIA Saclay
Pre-print Media Attached
02:00
15m
Talk
Experience Report: Domain Modeling with F# (short talk)
ML 2021
Scott Wlaschin None
Media Attached File Attached
02:15
15m
Talk
Isomorphisms are back! (short talk)
ML 2021
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 2021
Allister Beharry None
Media Attached File Attached
02:45
15m
Talk
A Data-centered User Study for jsCoq (short talk)
ML 2021
Hanneli Tavante McGill University
File Attached

Thu 26 Aug

Displayed time zone: Seoul change

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

ML 2021

Semantics & Verification

ML 2021

Compiler & Language Correctness

ML 2021

Keynote

ML 2021

Language & Library Design

Fri 27 Aug

Displayed time zone: Seoul change

Room1:00302:0030
ML

ML 2021

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