Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Nicolas Oury
Since November 2006, I am a Marie Curie research fellow in the Foundations of Programming Group of the University of Nottingham.
I am interested in Type Theory and programming with dependent types, and I am involved in the development of Epigram 2 and PiSigma.
I am also writing dependently typed programs and studying the right design choices for Domain Specific Embedded Type systems.
Together with Conor McBride and Peter Morris, we are developping Ecce, the interface to the Proof State of the forthcoming Epigram 2. Ecce is currently usable even if it is still rough and neeed to be improved. It already has all the features of Epigram 2, including Observational Type Theory and Generic Programming.
Together with Wouter Swierstra, we are working on the embedding of domain specific language and type systems in a generic purpose dependently typed language. We have already embedded a Cryptol like language, a File Format system and a database interface within the Agda2 language. The paper has been presented at ICFP '08.
We are currently working on other applications of the same design patterns, to extend this paper to a longer version.
Publications
The Power Of Pi, [.pdf], with Wouter Swierstra , presented at ICFP 08.
In this paper, we exhibit the power of programming with dependent types by embedding different domain-specific languages into a general purpose dependently typed language. Each of these domain-specific languages demonstrates different design patterns for programming with dependent types. Documenting these techniques paves the way for further research in domain-specific type systems.
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and very well integrated inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.
Pattern matching coverage checking with dependent types using set approximations. [.pdf],
published in PLPV'07
proceedings.
In a dependently typed programming language, some cases can become useless in a pattern matching. Detecting such cases is undecidable in general. In this paper, we study a heuristic to detect some useless cases in a pattern matching. This heuristic consists in computing over-approximations of the set of inhabitants of inductive families of types, and keeping track of the link between indices and inhabitants.
Egalite et filtrage avec types dependants dans le Calcul des Constructions Inductives [.pdf], in French.
My Ph.D. thesis written under the
supervision by Christine
Paulin
in the Demons team
at LRI.
This is about equalities, extensionality and improved pattern matching in
the Calculus of Inductive Constructions. If you are not interested in detailed proofs, long aknowledgments or practising French, you shouldn't read this, but the other papers.
Extensionality in the
Calculus
of Constructions [.pdf
| slides.pdf],
published in TPHOL'05.
proceedings
We
present in this
paper some limitations of the conversion of the Calculus of Inductive
Constructions. These limitations can be removed by adding proved
equalities in the conversion. This is called extensionality. We
introduce an Extensional Calculus of Constructions and exhibit a
constructive translation of this system to a slight extension of the
Calculus of Inductive Constructions.
Observational
equivalence and program extraction in the Coq proof assistant [.ps.gz | slides.pdf],
published in TLCA'03 proceedings.
One
limitation of data structures written in the Coq proof assistant is
that they have to be purely functional. In this paper we introduce the
idea of using a purely functional data structure during development of
proofs and extract them using a persistant data structure, that is a
data structure that behaves like a purely functional one but may be
more performant. To formalize this in the Coq proof assistant, we use a
formalization of observational equivalence.