We present a type system with subtyping for first-class delimited continuations that
generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit …

We present direct proofs of termination of evaluation for typed delimited-control operators
shift and reset using a variant of Tait's method with context-based reducibility predicates. We …

The CPS hierarchy of Danvy and Filinski is a hierarchy of continuations that allows for
expressing nested control effects characteristic of, eg, non-deterministic programming or …

We present new proofs of termination of evaluation in reduction semantics (ie, a small-step
operational semantics with explicit representation of evaluation contexts) for System F with …

We present a method for mechanically obtaining certified one-pass, higher-order
transformations of lambda terms into continuation-passing style. Given a naive, non …

Certified programming is a framework in which any program is correct by construction. Proof
assistants and dependently typed programming languages are the representatives of this …

The Curry-Howard isomorphism relates systems of formal logic to models of computation. It
broadly states that proofs correspond to programs and formulae to types. For a long time it …

It is well known that the computational content of a termination proof of a calculus is an
interpreter that computes the result of an input term. Traditionally, such extraction has been …

Moje najważniejsze osiągnięcia naukowe dotyczą semantyki języków programowania
wyższego rzędu z kontynuacjami oraz jej zastosowań w zakresie implementacji języków …

W pracy pokazaliśmy, że nie istnieje algorytm rozstrzygający, czy dla danego zbioru T
zależności bazodanowych (Tuple Generating Dependencies) algorytm T-Chase zatrzyma …