A logical foundation for session-based concurrent computation

Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.

La logique et les logiques : la question du pluralisme

Partant des travaux séminaux de Boole, Frege et Russell, le mémoire cherche à clarifier l‟enjeu du pluralisme logique à l‟ère de la prolifération des logiques non-classiques et des développements en informatique théorique et en théorie des preuves. Deux chapitres plus « historiques » sont à l‟ordre du jour : (1) le premier chapitre articule l‟absolutisme de Frege et Russell en prenant soin de montrer comment il exclut la possibilité d‟envisager des structures et des logiques alternatives; (2) le quatrième chapitre expose le chemin qui mena Carnap à l‟adoption de la méthode syntaxique et du principe de tolérance, pour ensuite dégager l‟instrumentalisme carnapien en philosophie de la Logique et des mathématiques. Passant par l‟analyse d‟une interprétation intuitive de la logique linéaire, le deuxième chapitre se tourne ensuite vers l‟établissement d‟une forme logico-mathématique de pluralisme logique à l‟aide de la théorie des relations d‟ordre et la théorie des catégories. Le troisième chapitre délimite le terrain de jeu des positions entourant le débat entre monisme et pluralisme puis offre un argument contre la thèse qui veut que le conflit entre logiques rivales soit apparent, le tout grâce à l‟utilisation du point de vue des logiques sous-structurelles. Enfin, le cinquième chapitre démontre que chacune des trois grandes approches au concept de conséquence logique (modèle-théorétique, preuve-théorétique et dialogique) forme un cadre suffisamment général pour établir un pluralisme. Bref, le mémoire est une défense du pluralisme logique.

Analyse de la structure logique des inférences légales et modélisation du discours juridique

Thèse par articles.

Science and technology policies in open economies: the case of Latin America and the Caribbean

Includes bibliography

O realismo mágico na comunhão estética entre Memorial do convento e Cem anos de solidão

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Extending Implicit Computational Complexity and Abstract Machines to Languages with Control

The Curry-Howard isomorphism is the idea that proofs in natural deduction can be put in correspondence with lambda terms in such a way that this correspondence is preserved by normalization. The concept can be extended from Intuitionistic Logic to other systems, such as Linear Logic. One of the nice conseguences of this isomorphism is that we can reason about functional programs with formal tools which are typical of proof systems: such analysis can also include quantitative qualities of programs, such as the number of steps it takes to terminate. Another is the possiblity to describe the execution of these programs in terms of abstract machines. In 1990 Griffin proved that the correspondence can be extended to Classical Logic and control operators. That is, Classical Logic adds the possiblity to manipulate continuations. In this thesis we see how the things we described above work in this larger context.

The Finite Embeddability Property for some noncommutative knotted varieties of RL and DRL.

Residuated lattices, although originally considered in the realm of algebra providing a general setting for studying ideals in ring theory, were later shown to form algebraic models for substructural logics. The latter are non-classical logics that include intuitionistic, relevance, many-valued, and linear logic, among others. Most of the important examples of substructural logics are obtained by adding structural rules to the basic logical calculus

Production et articulation des appartenances au mouvement Slow Fashion sur Twitter

Ce mémoire explore les productions et les articulations des appartenances au mouvement Slow Fashion sur Twitter. En réaction au modèle actuel prédominant du Fast Fashion, basé sur une surproduction et une surconsommation des vêtements, le Slow Fashion sensibilise les différents acteurs du secteur de la mode à avoir une vision plus consciente des impacts de leurs pratiques sur les travailleurs, les communautés et les écosystèmes (Fletcher, 2007) et propose une décélération des cycles de production et de consommation des vêtements. L’enjeu de cette recherche est de montrer que le Slow Fashion se dessine notamment à travers les relations entres les différents acteurs sur Twitter et que l'ensemble de ces interactions prend la forme d'un rhizome, c’est-à-dire d’un système dans lequel les éléments qui le composent ne suivent aucune arborescence, aucune hiérarchie et n’émanent pas d’un seul point d’origine. (Deleuze & Guattari, 1976) Sur Twitter, les appartenances au Slow Fashion font surface, se connectent les unes aux autres par des liens de nature différente. Consommateurs, designers, entreprises, journalistes, etc., ces parties prenantes construisent collectivement le Slow Fashion comme mouvement alternatif à la mode mainstream actuelle. Mon cadre théorique s’est construit grâce à une analyse de la littérature des concepts de mode, d’identité et d’appartenance afin de mieux appréhender le contexte dans lequel le mouvement a émergé. Puis, j’ai également réalisé une étude exploratoire netnographique sur Twitter au cours de laquelle j’ai observé, tout en y participant, les interactions sur la plateforme abordant le Slow Fashion et/ou la mode éthique. Publiée sur ce blogue (http://belongingtoslowfashion.blogspot.ca), cette « creative presentation of research » (Chapman & Sawchuk, 2012) ne constitue pas une histoire présentant les prétendues origines de ce mouvement mais plutôt une photographie partielle à un certain moment du Slow Fashion. Construite tel un rhizome, elle n’a ni début, ni fin, ni hiérarchie. J’invite alors les lectrices/lecteurs à choisir n’importe quelle entrée et à délaisser toute logique linéaire et déductive. Cette exploration sera guidée par des liens hypertextes ou des annotations qui tisseront des connexions avec d’autres parties ou feront émerger d’autres questionnements. Il s’agit d’offrir une introduction aux enjeux que pose le Slow Fashion, d’ouvrir la voie à d’autres recherches et d’autres réflexions, ou encore de sensibiliser sur ce sujet.

Production et articulation des appartenances au mouvement Slow Fashion sur Twitter

Ce mémoire explore les productions et les articulations des appartenances au mouvement Slow Fashion sur Twitter. En réaction au modèle actuel prédominant du Fast Fashion, basé sur une surproduction et une surconsommation des vêtements, le Slow Fashion sensibilise les différents acteurs du secteur de la mode à avoir une vision plus consciente des impacts de leurs pratiques sur les travailleurs, les communautés et les écosystèmes (Fletcher, 2007) et propose une décélération des cycles de production et de consommation des vêtements. L’enjeu de cette recherche est de montrer que le Slow Fashion se dessine notamment à travers les relations entres les différents acteurs sur Twitter et que l'ensemble de ces interactions prend la forme d'un rhizome, c’est-à-dire d’un système dans lequel les éléments qui le composent ne suivent aucune arborescence, aucune hiérarchie et n’émanent pas d’un seul point d’origine. (Deleuze & Guattari, 1976) Sur Twitter, les appartenances au Slow Fashion font surface, se connectent les unes aux autres par des liens de nature différente. Consommateurs, designers, entreprises, journalistes, etc., ces parties prenantes construisent collectivement le Slow Fashion comme mouvement alternatif à la mode mainstream actuelle. Mon cadre théorique s’est construit grâce à une analyse de la littérature des concepts de mode, d’identité et d’appartenance afin de mieux appréhender le contexte dans lequel le mouvement a émergé. Puis, j’ai également réalisé une étude exploratoire netnographique sur Twitter au cours de laquelle j’ai observé, tout en y participant, les interactions sur la plateforme abordant le Slow Fashion et/ou la mode éthique. Publiée sur ce blogue (http://belongingtoslowfashion.blogspot.ca), cette « creative presentation of research » (Chapman & Sawchuk, 2012) ne constitue pas une histoire présentant les prétendues origines de ce mouvement mais plutôt une photographie partielle à un certain moment du Slow Fashion. Construite tel un rhizome, elle n’a ni début, ni fin, ni hiérarchie. J’invite alors les lectrices/lecteurs à choisir n’importe quelle entrée et à délaisser toute logique linéaire et déductive. Cette exploration sera guidée par des liens hypertextes ou des annotations qui tisseront des connexions avec d’autres parties ou feront émerger d’autres questionnements. Il s’agit d’offrir une introduction aux enjeux que pose le Slow Fashion, d’ouvrir la voie à d’autres recherches et d’autres réflexions, ou encore de sensibiliser sur ce sujet.

A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic

The clausal resolution method for propositional linear-time temporal logic is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. In this paper, we show how the normal form can be radically simplified, and consequently, how a simplified clausal resolutioin method can be defined for this impoprtant variety of logics.

Linear temporal logic and z refinement

Since Z, being a state-based language, describes a system in terms of its state and potential state changes, it is natural to want to describe properties of a specified system also in terms of its state. One means of doing this is to use Linear Temporal Logic (LTL) in which properties about the state of a system over time can be captured. This, however, raises the question of whether these properties are preserved under refinement. Refinement is observation preserving and the state of a specified system is regarded as internal and, hence, non-observable. In this paper, we investigate this issue by addressing the following questions. Given that a Z specification A is refined by a Z specification C, and that P is a temporal logic property which holds for A, what temporal logic property Q can we deduce holds for C? Furthermore, under what circumstances does the property Q preserve the intended meaning of the property P? The paper answers these questions for LTL, but the approach could also be applied to other temporal logics over states such as CTL and the mgr-calculus.

Non-Linear Network-Flow Model of Lukasiewicz’s Multivalue Logic

The paper presents a new network-flow interpretation of Łukasiewicz’s logic based on models with an increased effectiveness. The obtained results show that the presented network-flow models principally may work for multivalue logics with more than three states of the variables i.e. with a finite set of states in the interval from 0 to 1. The described models give the opportunity to formulate various logical functions. If the results from a given model that are contained in the obtained values of the arc flow functions are used as input data for other models then it is possible in Łukasiewicz’s logic to interpret successfully other sophisticated logical structures. The obtained models allow a research of Łukasiewicz’s logic with specific effective methods of the network-flow programming. It is possible successfully to use the specific peculiarities and the results pertaining to the function ‘traffic capacity of the network arcs’. Based on the introduced network-flow approach it is possible to interpret other multivalue logics – of E.Post, of L.Brauer, of Kolmogorov, etc.

Assembling a consistent set of sentences in relational probabilistic logic with stochastic independence

We examine the representation of judgements of stochastic independence in probabilistic logics. We focus on a relational logic where (i) judgements of stochastic independence are encoded by directed acyclic graphs, and (ii) probabilistic assessments are flexible in the sense that they are not required to specify a single probability measure. We discuss issues of knowledge representation and inference that arise from our particular combination of graphs, stochastic independence, logical formulas and probabilistic assessments. (C) 2007 Elsevier B.V. All rights reserved.

Probabilistic logic with independence

This paper investigates probabilistic logics endowed with independence relations. We review propositional probabilistic languages without and with independence. We then consider graph-theoretic representations for propositional probabilistic logic with independence; complexity is analyzed, algorithms are derived, and examples are discussed. Finally, we examine a restricted first-order probabilistic logic that generalizes relational Bayesian networks. (c) 2007 Elsevier Inc. All rights reserved.