Étienne Miquey

Normalization and continuation-passing-style interpretation of simply-typed call-by-need λ-calculus with control

2017 · HAL (Le Centre pour la Communication Scientifique Directe)

Ariola et al defined a call-by-need λ-calculus with control, together with a sequent calculus presentation of it. They mechanically derive from the sequent calculus presentation a continuation-passing-style transformation simulating the reduction. In this paper, we …

Dependent Type Theory in Polarised Sequent Calculus (abstract)

2020 · HAL (Le Centre pour la Communication Scientifique Directe)

(conference cancelled due to events)