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
Coadvised
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 FineGrained Evaluation
Strategy for DelimitedControl Operators shift0/dollar,
2022

Konrad Werbliński
Implementation of a Compiler
and a Virtual Machine for a Programming Language with
Algebraic Effects, 2022
Coadvised 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 ObjectOriented 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
NormalizationbyEvaluation Algorithm for MartinLöf
Type Theory, 2016

Piotr Polesiuk
Strong Normalization of System
Fbounded: 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
Gmachine 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
MLFamily Functional Language Using the LLVM Compiler
Infrastructure, 2018
