@incollection{boespflug_taichi:_2007,
title = {{TaiChi:} how to check your types with serenity},
volume = {9},
url = {http://www.haskell.org/sitewiki/images/5/5d/TMR-Issue9.pdf},
abstract = {A technical piece about my participation in the Google Summer of Code 2007 program.},
booktitle = {The {Monad.Reader}},
author = {Boespflug, Mathieu},
editor = {Swierstra, Wouter},
month = nov,
year = {2007},
keywords = {homepage},
pages = {17--31}
}
@inproceedings{boespflug_self-interpreters_2009,
address = {Los Angeles, California},
title = {From self-interpreters to normalization by evaluation},
url = {papers/nbe09b.pdf},
abstract = {We characterize normalization by evaluation as the composition of a self-interpreter with a self-reducer using a special representation scheme, in the sense of Mogensen (1992). We do so by deriving in a systematic way an untyped normalization by evaluation algorithm from a standard interpreter for the \${\textbackslash}lambda\$-calculus. The derived algorithm is not novel and indeed other published algorithms may be obtained in the same manner through appropriate adaptations to the representation scheme.},
booktitle = {Informal Proceedings of the 2009 Workshop on Normalization by Evaluation},
author = {Boespflug, Mathieu},
month = aug,
year = {2009},
keywords = {homepage},
pages = {29--34}
}
@inproceedings{boespflug_conversion_2010,
address = {Madrid, Spain},
title = {Conversion by evaluation},
url = {papers/padl10.pdf},
doi = {10.1007/978-3-642-11503-5_7},
abstract = {We show how testing convertibility of two types in dependently typed systems can advantageously be implemented instead untyped normalization by evaluation, thereby reusing existing compilers and runtime environments for stock functional languages, without peeking under the hood, for a fast yet cheap system in terms of implementation effort.
Our focus is on performance of untyped normalization by evaluation. We demonstrate that with the aid of a standard optimization for higher order programs (namely uncurrying), the reuse of native datatypes and pattern matching facilities of the underlying evaluator, we may obtain a normalizer with little to no performance overhead compared to a regular evaluator.},
booktitle = {Proceedings of the Twelfth Internation Symposium on Pracical Aspects of Declarative Languages},
author = {Boespflug, Mathieu},
month = jan,
year = {2010},
note = {A preliminary version was presented at the {NbE'09} workshop.},
keywords = {homepage}
}
@phdthesis{boespflug_conception_2011,
address = {Palaiseau},
title = {Conception d'un noyau de vérification de preuves pour le lambda-Pi-calcul modulo},
url = {papers/thesis.pdf},
school = {École Polytechnique},
author = {Boespflug, Mathieu},
month = jan,
year = {2011}
}
@inproceedings{boespflug_coqine:_2012,
address = {Manchester, {UK}},
series = {{CEUR} Workshop Proceedings},
title = {{CoqInE:} Translating the Calculus of Inductive Constructions into the lambda-Pi-calculus Modulo},
volume = {878},
url = {http://ceur-ws.org/Vol-878/paper3.pdf},
booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving},
author = {Boespflug, Mathieu and Burel, Guillaume},
month = jun,
year = {2012},
pages = {44--50}
}
@inproceedings{boespflug_lambda-pi-calculus_2012,
address = {Manchester, {UK}},
series = {{CEUR} Workshop Proceedings},
title = {The lambda-Pi-calculus Modulo as a Universal Proof Language},
volume = {878},
url = {http://ceur-ws.org/Vol-878/paper2.pdf},
booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving},
author = {Boespflug, Mathieu and Carbonneaux, Quentin and Hermant, Olivier},
month = jun,
year = {2012},
pages = {28--43}
}
@inproceedings{boespflug_full_2011,
series = {Lecture Notes in Computer Science},
title = {Full Reduction at Full Throttle},
volume = {7086},
url = {papers/cpp11.pdf},
doi = {10.1007/978-3-642-25379-9_26},
abstract = {Emerging trends in proof styles and new applications of interactive proof assistants exploit the computational facilities of the provided proof language, reaping enormous benefits in proof size and convenience to the user. However, the resulting proof objects really put the proof assistant to the test in terms of computational time required to check them. We present a novel translation of the terms of the full Calculus of {(Co)Inductive} Constructions to {OCaml} programs. Building on this translation, we further present a new fully featured version of Coq that offloads much of the computation required during proof checking to a vanilla, state of the art and fine tuned compiler. This modular scheme yields substantial performance improvements over existing systems at a reduced implementation cost. The work presented here builds on previous work described in [11], but we place particular emphasis in this paper on the fact that this scheme is in fact an instance of untyped normalization by evaluation [8, 14, 1,4].},
booktitle = {Certified Programs and Proofs},
author = {Boespflug, Mathieu and Dénès, Maxime and Grégoire, Benjamin},
editor = {Jouannaud, Jean-Pierre and Shao, Zhong},
year = {2011},
pages = {362--377},
file = {full_throttle.pdf:/home/mboes/.zotero/storage/MC4GEABH/full_throttle.pdf:application/pdf}
}
@inproceedings{boespflug_multi-level_2011,
title = {Multi-level Contextual Type Theory},
url = {http://arxiv.org/abs/1111.0087},
doi = {10.4204/EPTCS.71.3},
abstract = {Contextual type theory distinguishes between bound variables and meta-variables to write potentially incomplete terms in the presence of binders. It has found good use as a framework for concise explanations of higher-order unification, characterize holes in proofs, and in developing a foundation for programming with higher-order abstract syntax, as embodied by the programming and reasoning environment Beluga. However, to reason about these applications, we need to introduce meta{\textasciicircum}2-variables to characterize the dependency on meta-variables and bound variables. In other words, we must go beyond a two-level system granting only bound variables and meta-variables. In this paper we generalize contextual type theory to n levels for arbitrary n, so as to obtain a formal system offering bound variables, meta-variables and so on all the way to meta{\textasciicircum}n-variables. We obtain a uniform account by collapsing all these different kinds of variables into a single notion of variabe indexed by some level k. We give a decidable bi-directional type system which characterizes beta-eta-normal forms together with a generalized substitution operation.},
booktitle = {Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice},
author = {Boespflug, Mathieu and Pientka, Brigitte},
month = oct,
year = {2011},
note = {{EPTCS} 71, 2011, pp. 29-43},
keywords = {Computer Science - Logic in Computer Science, Computer Science - Programming Languages},
file = {1111.0087 PDF:/home/mboes/.zotero/storage/RQPIURNU/Boespflug et Pientka - 2011 - Multi-level Contextual Type Theory.pdf:application/pdf}
}
This file was generated by bibtex2html 1.97.