ﻻ يوجد ملخص باللغة العربية
We develop a denotational semantics of Linear Logic with least and greatest fixed points in coherence spaces (where both fixed points are interpreted in the same way) and in coherence spaces with totality (where they have different interpretations). These constructions can be carried out in many different denotational models of LL (hypercoherences, Scott semantics, finiteness spaces etc). We also present a natural embedding of G{o}del System T in LL with fixed points thus enforcing the expressive power of this system as a programming language featuring both normalization and a huge expressive power in terms of data types.
We develop a denotational semantics of muLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baeldes propositional muMALL with exponentials. Our general categorical setting is based on the notion of Seely
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for propositional intuitionistic logic, in which proofs are factorised in a
The word problem for categories with free products and coproducts (sums), SP-categories, is directly related to the problem of determining the equivalence of certain processes. Indeed, the maps in these categories may be directly interpreted as proce
We describe a mathematical structure that can give extensional denotational semantics to higher-order probabilistic programs. It is not limited to discrete probabilities, and it is compatible with integration in a way the models that have been propos
Higher-order recursion schemes are recursive equations defining new operations from given ones called terminals. Every such recursion scheme is proved to have a least interpreted semantics in every Scotts model of lambda-calculus in which the termina