Nous proposons dans ce manuscrit un nouveau cadre sémantique, basé sur la composition de variantes Linéaires de la réalisabiblité de Krivine et du forcing de Cohen. Le premier ingrédient est la Monitoring Abstract Machine : un environnement de calcul qui utilise des cases mémoires réservées utilisées pour "surveiller" l'exécuter des programmes, dans le style de la KFAM introduite par Miquel. Cette machine émerge naturellement d'une transformation de programme basée sur un forcing Linéaire. Nous introduisons par la suite la notion centrale d'Algèbre de Monitoring et le modèle de réalisabiblité associé. Chaque algèbre de monitoring induit une sémantique correcte pour un langage de programmation associé. Nous utilisons ensuite la technique de forcing itéré pour combiner plusieurs algèbres de monitoring. Nous montrons que la structure de forcing peut être utilisée pour représenter la consommation de ressources (en particulier le temps), le step-indexing ou encore des références d'ordre supérieur. Nous appliquons notre théorie pour obtenir trois preuves de corrections complexes : - Nous donnons la première preuve sémantique de la cohérence d'une théorie des ensembles naïve sans contraction introduite par Grishin. - Nous utilisons notre cadre pour obtenir un résultat de terminaison en temps polynomial pour un langage de programmation avec types récursifs basé sur une logique light. - Nous reprouvons la correction d'un langage avec références d'ordre supérieur et mise à jour forte, inspiré par un système de type introduit par Ahmed et al. / In this thesis, we are interested in semantical proof of correctness results for complex programming languages. We advocate the need for a theoretical framework that allows one to build realizability semantics using basic blocks and use algebraic constructions to combine those blocks. We propose a framexork based on the composition of Linear variants of Krivine realizability and Cohen forcing. The first ingredient of environment that prossesses special memory cells used to monitor the execution of programs, in the style of Miquel's KFAM. It is shown how this new machine emerges from a Linear forcing program transformation. We then introduce the central notionof Monitoring Algebra and the associated realizability interpretation. Different monitoring algebras induce sound semantics of different programing languages. We then present an algebraic construction to combine different Monitoring Algebras based on the techniuqe of forcing iteration. We show that the forcing structure can be used to represent the consumption or resources, in particular time, but also step-indexing or the use of higher-order references. We finally apply our results to retrieve three complex soundness results : - We give the first semantical proof of the consistency of a contraction-free nave set theory, originally introduced by Grishin. - Wuse our framework to obtain a polynomial time terminationresult for a light-logic based programming language featuring recursive types. - We reprove to soundness of a language with references that supports strong updates, based on a Linear type system inspired by a workof Ahmed et al.

No description available.

I argue that satisfaction and reference—and therefore, truth—are multiply realizable properties. I advocate a novel approach motivated by a commitment to the robustness and fruitfulness of truth-theoretic approaches to natural language semantics. DEFLATIONISM: Philosophers keen on deflating the metaphysical pretensions of truth theories claim that we need not appeal to a substantive truth-property. Recently, however, some philosophers have sought to combine deflationism about truth with the view that our concept of truth or the truth-predicate can play an important role in natural language semantics. TRUTH-THEORETIC SEMANTICS: The goal of a formal semantic theory of a natural language is to provide both the semantic values of that language’s lexically primitive items as well as the semantically significant modes of combining those basic elements into meaningful and more complex expressions. Most approaches have in common a commitment to finite stateability and compositionality as well as a commitment to something like Davidson’s “Convention T.” PLURALISM: Pluralists about truth argue that different areas of discourse have different truth-properties. Can pluralism successfully be combined with a commitment to truth-theoretic semantics? OPEN SEMANTIC FUNCTIONALISM: The pluralist approaches to truth are unsatisfactory for a variety of reasons. The only option, I argue, is to regard truth as multiply-realizable. Specifically, we should view the set of truth’s realizers as possessing non-actual members—as being “open.” Truth is defined in the usual way in terms of reference and satisfaction, but these latter two relations are to be understood as multiply realizable but open. The property of truth can be specified using the Ramsey/Lewis method. My final view—Open Semantic Functionalism—respects compositionality and finite stateability, avoids triviality, handles plurality, and fits with robust, explanatorily significant natural language semantic theories.

In this thesis we construct an analogue in tropical geometry for a class of Schubert varieties from classical geometry. In particular, we look at the collection of tropical lines contained in the fan tropical plane. We call these tropical spaces "tropical Schubert prevarieties", and develop them after creating a tropical analogue for flag varieties that we call the "flag Dressian". Having constructed this tropical analogue of Schubert varieties we then determine that the 2-skeleton of these tropical Schubert prevarieties is realizable. In fact, as long as the lift of the fan tropical plane is in general position, only the 2-skeleton of the tropical Schubert prevariety is realizable. / text

Type identity theory is a theory within physicalism that maintains that types of mental states or processes are identical to types of states or processes in the brain. This would imply mental types can’t be encountered in physical structures other than the brain. But it seems to be the case that other biological creatures with different physical processes going on in their brain are able to experience a mental state such as pain. Even our brain, with its ability to undergo modification, functionally and structurally, in response to experience or injury, an ability called neuroplasticity, seems to have the ability to instantiate or realize the same mental state by two different neural events. This is the multiple realizability nature of the mental, that challenge type identity theory, but that functionalism seems to account for. Multiple realizability seems to provide a plausible basis for the irreducibility of mind to brain, and thus a good argument for why they should not be considered identical. I argue that when type identity theory claims that types of mental states or processes are identical to types of states or processes in the brain, this should be understood as claiming that types of mental states are identical to types of mechanisms in the brain, by which I mean types of interaction between fundamental particles that comprises the brain. I argue that two physical structures realizing the same mental state must be relevantly similar in the way their respective fundamental particles are interacting with one another. In other words, that similarity in function implies similarity in the way the physical realizers are organized. Therefore, the multiple realizability nature of mental states shouldn’t render them irreducible or non-identical to specific types of interactions fundamental particles.

It has been argued that there are physically different ways of instantiating mental properties, the nature of which is the subject matter of cognitive science. This claim has been known as the Multiple Realizability Thesis (MRT). It has been suggested that the MRT shows that a reduction of mental properties to physical properties is impossible, as there cannot be one-to-one correspondences of mental properties to the properties of the brain. Moreover, it has been argued that the latter point shows that physical explanations are not relevant to the explanations of cognitive science, as they would lack the generality of psychological explanations. This thesis will try to explain from which assumptions of a traditional cognitive science perspective the MRT follows. It will also discuss several responses that have been introduced against both the MRT and the anti-reductionist conclusions that are assumed to follow from it. The responses include a challenge to the scientific status of cognitive science. According to this challenge, the MRT entails that the subject matter of cognitive science, namely mental properties, lack a similarity in the physical level, hence an instance of a mental property is not informative about another instance. While discussing these theories, a revision of the MRT will be proposed. According to this revision, the MRT is compatible with the assumption that there could be an underlying similarity between different physical realizers of a given mental property. It will be argued that by means of this revision, both the challenge to the scientific status of cognitive science, and the argument for the irrelevance of physical explanations will fail.

This thesis focuses on the computational interpretation of Cohen's forcing through the classical Curry-Howard correspondence, using the tools of classical realizability. In a first part, we start by a general introduction to classical realizability in second-order arithmetic (PA2). We cover the description of the Krivine Abstract Machine (KAM), the construction of the realizability models, the realizers for arithmetic and the main two computational topics: specification and witness extraction. To illustrate the flexibility of this approach, we show that it can be effortlessly adapted to several extensions such as new instructions in the KAM or primitive datatypes like natural, rational and real numbers. These various works are formalized in the Coq proof assistant.In the second part, we redesign this framework in a higher-order setting and compare it to PA2.This change is necessary to fully express the forcing transformation, but it also allows us to uniformize the theory and integrate all datatypes. We present forcing in classical realizability, initially due to Krivine, and extend it to generic filters whenever the forcing conditions form a datatype. We can then see forcing as a program transformation adding a memory cell with its access primitives. Our aim is to find more efficient realizers rather than independence results, which are the common use of forcing techniques. The methodology is illustrated on the example of Herbrand's theorem, the proof by forcing of which gives a much more efficient program than the usual proof. Furthermore, we can recover the natural algorithm that one can write to solve the underlying computational problem if we use a datatype as forcing poset.

Au cours des dernières années, les assistants de preuves on fait des progrès considérables et ont atteint un grand niveau de maturité. Ils ont permit la certification de programmes complexes tels que des compilateurs et même des systèmes d'exploitation. Néanmoins, l'utilisation d'un assistant de preuve requiert des compétences techniques très particulières, qui sont très éloignées de celles requises pour programmer de manière usuelle. Pour combler cet écart, nous entendons concevoir un langage de programmation de style ML supportant la preuve de programmes. Il combine au sein d'un même outil la flexibilité de ML et le fin niveau de spécification offert par un assistant de preuve. Autrement dit, le système peut être utilisé pour programmer de manière fonctionnelle et fortement typée tout en autorisant l'obtention de nouvelles garanties au besoin.On étudie donc un langage en appel par valeurs dont le système de type étend une logique d'ordre supérieur. Il comprend un type égalité entre les programmes non typés, un type de fonction dépendant, la logique classique et du sous-typage. La combinaison de l'appel par valeurs,des fonctions dépendantes et de la logique classique est connu pour poser des problèmes de cohérence. Pour s'assurer de la correction du système (cohérence logique et sûreté à l'exécution), on propose un cadre théorique basé sur la réalisabilité classique de Krivine. La construction du modèle repose sur une propriété essentielle qui lie les différent niveaux d'interprétation des types d'une manière novatrice.On démontre aussi l'expressivité de notre système en se basant sur son implantation dans un prototype. Il peut être utilisé pour prouver des propriétés de programmes standards tels que la fonction « map »sur les listes ou le tri par insertion. / In recent years, proof assistant have reached an impressive level of maturity. They have led to the certification of complex programs such as compilers and operating systems. Yet, using a proof assistant requires highly specialised skills and it remains very different from standard programming. To bridge this gap, we aim at designing an ML-style programming language with support for proofs of programs, combining in a single tool the flexibility of ML and the fine specification features of a proof assistant. In other words, the system should be suitable both for programming (in the strongly-typed, functional sense) and for gradually increasing the level of guarantees met by programs, on a by-need basis.We thus define and study a call-by-value language whose type system extends higher-order logic with an equality type over untyped programs, a dependent function type, classical logic and subtyping. The combination of call-by-value evaluation, dependent functions and classical logic is known to raise consistency issues. To ensure the correctness of the system (logical consistency and runtime safety), we design a theoretical framework based on Krivine's classical realisability. The construction of the model relies on an essential property linking the different levels of interpretation of types in a novel way.We finally demonstrate the expressive power of our system using our prototype implementation, by proving properties of standard programs like the map function on lists or the insertion sort.

Cette thèse s'intéresse à la correspondance de Curry-Howard classique et son interaction avec le forcing de Cohen, en s'appuyant sur les outils de la réalisabilité classique. Dans une première partie, nous commençons par une introduction générale à la réalisabilité classique dans PA2, avec pour fil directeur l'extraction de témoin. Cette introduction couvre la description de la machine abstraite de Krivine (KAM), la construction des modèles, la réalisation de l'arithmétique et les deux principales problématiques calculatoires : la spécification et l'extraction de témoin. Pour illustrer la flexibilité de ce cadre, nous montrons ensuite qu'il s'adapte sans effort à diverses extensions : l'ajout d'instructions supplémentaires dans la KAM ou l'introduction de types de données primitifs tels que les entiers, les rationnels et les réels. Ces divers travaux ont été formalisés dans l'assistant de preuves Coq.Dans une seconde partie, nous redéfinissons ce cadre à l'ordre supérieur et le comparons à PA2. Ce changement, nécessaire pour exprimer pleinement la transformation de forcing, uniformise la théorie et permet d'intégrer tous les types de données. Nous présentons ensuite le forcing en réalisabilité classique, initialement dû à Krivine, puis l'étendons aux filtres génériques, lorsque les conditions de forcing forment un type de données. Cela permet de relire le forcing comme une transformation de programmes, dans le but d'obtenir des réalisateurs plus efficaces plutôt que des résultats d'indépendance. Cette méthode est illustrée notamment par l'exemple du théorème de Herbrand, dont la preuve par forcing donne un programme nettement plus efficace que la preuve habituelle. / This thesis focuses on the computational interpretation of Cohen's forcing through the classical Curry-Howard correspondence, using the tools of classical realizability. In a first part, we start by a general introduction to classical realizability in second-order arithmetic (PA2). We cover the description of the Krivine Abstract Machine (KAM), the construction of the realizability models, the realizers for arithmetic and the main two computational topics: specification and witness extraction. To illustrate the flexibility of this approach, we show that it can be effortlessly adapted to several extensions such as new instructions in the KAM or primitive datatypes like natural, rational and real numbers. These various works are formalized in the Coq proof assistant.In the second part, we redesign this framework in a higher-order setting and compare it to PA2.This change is necessary to fully express the forcing transformation, but it also allows us to uniformize the theory and integrate all datatypes. We present forcing in classical realizability, initially due to Krivine, and extend it to generic filters whenever the forcing conditions form a datatype. We can then see forcing as a program transformation adding a memory cell with its access primitives. Our aim is to find more efficient realizers rather than independence results, which are the common use of forcing techniques. The methodology is illustrated on the example of Herbrand's theorem, the proof by forcing of which gives a much more efficient program than the usual proof. Furthermore, we can recover the natural algorithm that one can write to solve the underlying computational problem if we use a datatype as forcing poset.

This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery. / Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinatoriska algebror—för varje partiell kombinatorisk algebra finns det en motsvarande realiserbarhetstolkning. Jag konstruerar två partiella kombinatoriska algebror. En av dessa ger en realiserbarhetstolkning som är ekvivalent med Kleenes ursprungliga tolkning, men dess konstruktion använder inte det sedvanliga rekursionsteoretiska maskineriet.