WG meeting in Krakow
EUTypes meeting, Krakow, Poland, 23-24 February 2019, in relation to Lambda Days 2019
Accommodation information can be found here.
Venue
Katedra Informatyki AGH, D-17, Kawiory 21, Kraków. room 1.19
Registration
The meeting is open for free to all members of the EUTypes COST network as well as to all other researchers interested in the topic.
Invited speakers
- François Dupressoir, University of Surrey, UK
- Paolo Giarrusso, EPFL, Switzerland
- Robbert Krebbers, Delft University of Technology, Netherlands
- Kenji Maillard, INRIA, France
- Pierre-Yves Strub, École Polytechnique, France
Talks
François Dupressoir: A (somewhat) gentle introduction to machine-checked cryptographic proofs: privacy and verifiability for online voting.
Robbert Krebbers: Relational reasoning using concurrent separation logic
Paolo Giarrusso: Towards Semantic Type Soundness for Dependent Object Types and Scala with Logical Relations in Iris
Kenji Maillard: Designing Dijkstra Monads
Pierre-Yves Strub: High-Assurance and High-Speed Cryptography
Thorsten Altenkirch: Naturality for Free
András Kovács: Fast elaboration for dependent type theories
Maciej Bendkowski: Statistical properties and evaluation of random λ-terms -- a survey
Stefania Dumbrava: Certified Graph Query Processing
Denis Firsov: Efficient Mendler-Style Lambda-Encodings in Cedille
Léon Gondelman: Semi-Automated Reasoning About Non-Determinism in C Expressions
Serguei Lenglet: HOpi in Coq
Tiziana Margaria: Semantic Types Aid Behavioral Models to become Digital Twins spanning Software and Processes
Peter Podlovics: GRIN: Dead data elimination in the context of dependently typed languages
Willard Rafnsson: Types for Information-Flow Control in Functional Programming Languages
Aleksy Schubert: Formalisation of a frame stack semantics for a Java-like language
Program
23 Feb (Sat)
Session 1 Chair: Keiko Nakata
- 9:00 - 10:00: Relational reasoning using concurrent separation logic. "Robbert Krebbers". Abstract, slides
- 10:00 - 10:30: Break
Session 2 Chair: Robbert Krebbers
- 10:30 - 11:00: Semi-Automated Reasoning About Non-Determinism in C Expressions. "Léon Gondelman". Abstract, slides
- 11:00 - 11:30: Efficient Mendler-Style Lambda-Encodings in Cedille. "Denis Firsov". Abstract, slides
- 11:30 - 12:00: Formalisation of a frame stack semantics for a Java-like language. "Aleksy Schubert". Abstract
- 12:00 - 13:30: Lunch
Session 3 Chair: Pierre-Yves Strub
- 13:30 - 14:30: Towards Semantic Type Soundness for Dependent Object Types and Scala with Logical Relations in Iris. "Paolo Giarrusso". Abstract
- 14:30 - 15:00: Certified Graph Query Processing. "Stefania Dumbrava". Abstract, slides
- 15:00 - 15:30: Break
Session 4 Chair: Paolo Giarrusso
- 15:30 - 16:30: Designing Dijkstra Monads, "Kenji Maillard". Abstract, slides
- 16:30 - 17:00: Statistical properties and evaluation of random λ-terms -- a survey. "Maciej Bendkowski". Abstract, slides
- 17:00 - 17:30 Break
Session 5 Chair: András Kovács
- 17:30 - 18:00: Naturality for Free. "Thorsten Altenkirch". slides
- 18:00 - 18:30: Semantic Types Aid Behavioral Models to become Digital Twins spanning Software and Processes. "Tiziana Margaria". Abstract
24 Feb (Sun)
Session 1 Chair: Aleksy Schubert
- 9:00 - 10:00: High-Assurance and High-Speed Cryptography. "Pierre-Yves Strub". Abstract
- 10:00 - 10:30: Types for Information-Flow Control in Functional Programming Languages. "Willard Rafnsson". Abstract, slides
- 10:30 - 11:00: GRIN: Dead data elimination in the context of dependently typed languages. "Péter Dávid Podlovics". Abstract, slides
- 11:00 - 11:30: Break
Session 2 Chair: Kenji Maillard
- 11:30 - 12:00: Fast elaboration for dependent type theories. "András Kovács". Abstract, slides
- 12:00 - 12:30: HOpi in Coq. "Serguei Lenglet". Abstract, slides
- 12:30 - 13:30: A (somewhat) gentle introduction to machine-checked cryptographic proofs: privacy and verifiability for online voting. "François Dupressoir". Abstract, slides
Organisers
Aleksy Schubert, Warsaw University
Keiko Nakata, SAP SE
