1,721,028 research outputs found
Formalisation et Méta-Théorie de la Théorie des Types
No full textDans cette thèse, je parle de la méta-théorie de la théorie des types et de la façon de la formaliser dans un assistant de preuve. Je me concentre d’abord sur une traduction conservative de la théorie des types extensionnelle vers la théorie des types intensionnelle ou faible, entièrement écrite en Coq. La première traduction consiste en une suppression de la règle de reflection de l’égalité, tandis que la deuxième traduction produit quelque chose de plus fort : la théorie des types faibles est une théorie des types sans notion de conversion. Le résultat de conservativité implique que la conversion n’augmente pas la puissance logique de la théorie des types. Ensuite, je montre ma contribution au projet MetaCoq de formalisation et de spécification de Coq au sein de Coq. En particulier, j’ai travaillé sur l’implantation d’un vérificateur de type pour Coq, en Coq. Ce vérificateur de type est prouvé correct vis à vis de la spécification et peut être extrait en code OCaml et exécuté indépendamment du vérificateur de type du noyau de Coq. Pour que cela fonctionne, nous devons nous appuyer sur la métathéorie de Coq que nous développons, en partie, dans le projet MetaCoq. Cependant, en raison des théorèmes d’incomplétude de Gödel, nous ne pouvons pas prouver la cohérence de Coq dans Coq, ce qui signifie que certaines propriétés — principalement la forte normalisation — doivent être supposées, c’est-à-dire prises comme axiomes.In this thesis, I talk about the metatheory of type theory and about how to formalise it in a proof assistant. I first focus on a conservative translation between extensional type theory and either intensional or weak type theory, entierely written in Coq. The first translation consists in a removal of the reflection of equality rule, whereas the second translation produces something stronger: weak type theory is a type theory with no notion of conversion. The conservativity result implies that conversion doesn’t increase the logical power of type theories. Then, I show my work for the Meta- Coq project of formalising and specifying Coq within Coq. In particular I worked on writing a type-checker for Coq, in Coq. This type checker is proven sound with respect to the specification and can be extracted to OCaml code and run independently of Coq’s kernel type-checker. For this to work we have to rely on the meta-theory of Coq which we develop, in part, in the MetaCoq project. However, because of Gödel’s incompleteness theorems, we cannot prove consistency of Coq within Coq, and this means that some properties— mainly strong normalisation—have to be assumed, i.e. taken as axioms
Coq avec Classes
No full textNational audienceWe give an introduction to the type class system and show its use through a number of examples
Elaborations in Type Theory
No full textInternational audienceDependent Type Theory as implemented into proof assistants and programming languages like Coq and Agda provide a firm and general basis for the formalization of mathematics and computer software. However, the core dependent type theory exposes a rather spartan interface for programming and writing proofs. Over the years a number of higher-level constructs and techniques have been developed to overcome this difficulty without touching the core language. For instance, implicit syntax, tactics and meta-languages like Ltac have been used successfully to make systems more accessible, automatable and scalable. Our research investigates further elaborations from high-level languages into dependent type theory. We present three such elaborations that facilitate programming with proofs, inductive families and overloaded functions in the Coq proof assistant. We demonstrate their usefulness for defining objects and structuring developments, as well as their crucial help in proofs
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
A New Look at Generalized Rewriting in Type Theory
No full textRewriting is an essential tool for computer-based reasoning, both automated and assisted. This is because rewriting is a general notion that permits modeling a wide range of problems and provides a means to effectively solve them. In a proof assistant, rewriting can be used to replace terms in arbitrary contexts, generalizing the usual equational reasoning to reasoning modulo arbitrary relations. This can be done provided the necessary proofs that functions appearing in goals are congruent with respect to specific relations. We present a new implementation of generalized rewriting in the Coq proof assistant, making essential use of the expressive power of dependent types and the recently implemented type class mechanism. The new rewrite tactic improves on and generalizes previous versions by natively supporting higher-order functions, polymorphism and subrelations. The type class system inspired by Haskell provides a perfect interface between the user and the tactic, making it easily extensible
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
- …
