Steven Keuchel.
Ph.D. thesis, Doctor of Computer Science, Universiteit Gent, 2018
This thesis investigates code reuse as a means to reduce costs of programming language meta-theory mechanizations, specifically principled reuse via modularity and genericity. Read more
Dominique Devriese, Marco Patrignani, Frank Piessens and Steven Keuchel.
Published in Logical Methods in Computer Science, Volume 13, Issue 4, 2017
A common technique to proof compiler full-abstraction is based on the back-translation of target-level program contexts to behaviourally-equivalent source-level contexts. However, constructing such a backtranslation is problematic when the source language is not strong enough to embed an encoding of the target language. We propose a general and elegant solution for this problem. Read more
Steven Keuchel, Stephanie Weirich and Tom Schrijvers.
Published in Proceedings of the 25th European Symposium on Programming, 2016
A stumbling block for reuse in mechanizations is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte framework in the context of programming language meta-theory. This paper takes a better approach to the problem with datatype-generic programming. Read more
Steven Keuchel and Tom Schrijvers.
Draft submitted to the 18th ACM SIGPLAN international conference on Functional programming (ICFP'15), 2015
Nearly all meta-programming tools need to deal with binders in abstract syntax trees. Unfortunately, ubiquitous boilerplate functions for computing free variables and variable substitution are remarkably intricate and hard to get right. Our new specification language InBound brings much needed relief. Read more
Steven Keuchel, Stephanie Weirich and Tom Schrijvers.
Draft submitted to the 42th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'15), 2014
A key concern in the mechanization of programming language metatheory is the representation of terms with variable binding. We present a new solution to generically handle the boilerplate involved in mechanizations that scales to rich binding forms and advanced rules of scoping. Read more
Benjamin Delaware, Steven Keuchel, Tom Schrijvers and Bruno C. d. S. Oliveira.
Published in Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, 2013
This paper presents 3MT, a framework for modular mechanized meta-theory of languages with effects. Using 3MT, individual language features can be built separately and then reused to create different languages with fully mechanized meta-theory. Read more
Steven Keuchel and Tom Schrijvers.
Published in Proceedings of the 9th ACM SIGPLAN workshop on Generic programming, 2013
A stumbling block for reuse in mechanizations is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte framework in the context of programming language meta-theory. This paper takes a better approach to the problem with datatype-generic programming. Read more
Steven Keuchel and Johan T. Jeuring.
Published in Proceedings of the 8th ACM SIGPLAN workshop on Generic programming, 2012
This paper defines a datatype-generic universe to specify the binding and scoping structure of languages. Two interpretations of the universe are given: one based on parametric higher-order abstract syntax and one on well-typed de Bruijn indices. We also generically define a conversion of the former to the latter Read more
Steven Keuchel and Tom Schrijvers.
Published in Pre-Proceedings of the 24th International Symposium on Implementation and Application of Functional Languages, 2012
This paper shows a novel approach to modularly reason about higher-order functions that are polymorphic in a monad based on a judicious combination of the coroutine monad transformer and monad morphisms. Read more