print · source · login   

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