Students

Current PhD students:

• Mateusz Pyzik
  Research on the operational semantics of delimited control and algebraic effects
  

Former PhD students:

• Tomasz Drab
  Reduction Strategies in the Lambda Calculus and Their Implementation through Derivable Abstract Machines, 2022, submitted
  Co-advised with Małgorzata Biernacka
• Piotr Polesiuk
  Reasoning About Control Effects: From Program Equivalence to Language Design, 2021
• Marek Materzok
  Control Abstraction for Layered Continuations: Semantics, Types and Implementation, 2014

Current MSc students:

Former MSc students:

• Kamil Listopad
  A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar, 2022
• Konrad Werbliński
  Implementation of a Compiler and a Virtual Machine for a Programming Language with Algebraic Effects, 2022
  Co-advised with Filip Sieczkowski
• Gabriel Sztorc
  Formal Verification of Type Inference for a Minimal Fragment of Haskell Using the Coq Proof Assistant, 2022
• Maciej Buszka
  The Functional Correspondence Applied: An Implementation of a Semantics Transformer, 2020
• Łukasz Dąbek
  Böhm's Theorem in Lambda Calculi with Control Operators, 2019
• Mikołaj Nowak
  A Coq Formalization of a Type System for an Object-Oriented Programming Language, 2019
• Łukasz Czapliński
  The Application of Functional Programming to the Construction of a Visual Programming Environment, 2016
• Paweł Wieczorek
  A Formalization in Coq of the Normalization-by-Evaluation Algorithm for Martin-Löf Type Theory, 2016
• Piotr Polesiuk
  Strong Normalization of System F-bounded: A Proof by a Coercion Translation to System F, 2014
• Wojciech Jedynak
  Operational Semantics of Ltac: A Formal Study of the Tactic Language of the Coq Proof Assistant, 2013
• Jakub Korczyński
  The Forte Framework for Music Composition: Two EDSLs for Music Composition and Analysis, 2012
• Maciej Piróg
  Toward a Certified Haskell Compiler: Correctness and Implementation of the Spineless Tagless G-machine Verified in the Coq Proof Assistant, 2010
• Filip Sieczkowski
  Automated Derivation of Abstract Machines from Reduction Semantics: A Formalisation of the Refocusing Transformation in the Coq Proof System, 2010

Current BSc students:

Former BSc students:

• Wiktor Kuchta
  Normalization for Algebraic Effect Handlers, 2022
• Maciej Buszka
  Implementation of Static and Dynamic Semantics for a Calculus with Algebraic Effects and Handlers Using PLT Redex, 2019
  
• Mateusz Lewko
  An Implementation of a ML-Family Functional Language Using the LLVM Compiler Infrastructure, 2018