hkt: Florent Kirchner
Hey there. I am a post-doctoral fellow drawn to theoretical and applied research in computer science. I am working in the fields of formal methods and software security. More specifically I am interested in the rich interaction between proof systems, the design of proof languages and in deduction modulo.
Notes and Publications
This section regroups my recent bibliography with links to bibtex reference files and electronic editions when available. An exhaustive list of papers, organized by referring type, is available here.
- Constraint Based Strategies. [ee] [bib]
- Functional and Constraint Logic Programming, volume 5979 of Lecture Notes in Computer Science, 2010.
- Numerous computational and deductive frameworks use the notion of strategy to guide reduction and search space exploration, making the macro scale control of micro operations an explicit object of interest. In recent works, abstract strategies have been defined in extension but also intensionally. In this paper we complete these views with a new declarative approach based on constraints, which are used to model the different parts of a strategy. This procedure allows us to express elaborate strategies in a declarative and reusable way.
- System Support for Forensic Evidence. [ee] [bib]
- Advances in Digital Forensics V, volume 306 of IFIP Advances in Information and Communication Technology, 2009.
- If the discoveries of forensic analysts are to hold up to scrutiny in court, they must meet the standard for scientific evidence. Software systems are currently developed without consideration of this fact. We argue for the development of a formal framework for constructing digital artifacts that can serve as proxies for physical evidence, that is they are difficult to forge. A system so imbued will facilitate sound digital forensic inference. As a case study, we describe filesystem augmentation needed to transparently provide such support.
- Strategic Computations and Deductions. [ee] [bib]
- Reasoning in Simple Type Theory, volume 17 of Mathematical Logic and Foundations, 2008.
- In this paper we are contributing to the theoretical foundations of strategies and to the convergence of different points of view, namely rewriting-based computations on one hand, rule-based deduction and proof-search on the other hand. We will rely on previous works and strategy languages that have been recently designed and studied. In rewriting, from elementary strategies expressions directly issued from a term rewriting system R, more elaborated strategies expressions can be built using a strategy language. A similar mechanism also exists in proof systems, where a set of core strategies is used to program sophisticated proof search patterns.
More recent, yet-unpublished work include a journal article on the structure of dynamic proof interaction and a conference note on the design of a distributed proof system.
Software and Proofs
The Evidential Tool Bus takes a novel approach towards formal verification tools composition and interoperability, by relying on asynchronous message passing with a unified proof data store. This work was carried out during my postdoctoral visit at SRI International, and hasn't been made public yet.
fsp is a prototype proof assistant using sequent calculus logics and proof terms. It is designed to generate proof scripts for other formal tools, such as Coq and PVS. More information, and download options, are found on its website.
A library of real closed fields has been developped for fsp, using results in the theory of classes to encode second-order formulas in the prover's first-order framework. The documented specifications and proofs can be downloaded here.
Practicals is a PVS package that aims at defining a simple strategy language for the prover. Its implementation is based on a categorical construction, encoded as a datatype and associated functions, called a proof monad.
Contact
Paper-and-pigments mail will find me at:
| INRIA Rennes – Bretagne Atlantique, IRISA |
| Bureau F211 |
| Campus de Beaulieu |
| 35042 Rennes Cedex, France |
| +33 (0)29 984 7152 |
If you'd rather go digital, here is my electronic mail address, as a Lisp function:
(format nil "~a@~a" "florent.kirchner" "irisa.fr")
For all intents and purposes, my GPG key is available on the MIT servers, and locally.
Colophon
The body text is set 12/18px on a 510px measure with Helvetica. The source code of this website is available from github. Feel free to fork it, submit patches, and offer suggestions.