Related papers: Parametricity in an Impredicative Sort
We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality and the key properties of…
The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage…
Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that…
We present an extension of the second-order logic AF2 with iso-style inductive and coinductive definitions specifically designed to extract programs from proofs a la Krivine-Parigot by means of primitive (co)recursion principles. Our logic…
In our paper "Uniformity and the Taylor expansion of ordinary lambda-terms" (with Laurent Regnier), we studied a translation of lambda-terms as infinite linear combinations of resource lambda-terms, from a calculus similar to Boudol's…
Sequential propositional logic deviates from ordinary propositional logic by taking into account that during the sequential evaluation of a propositional statement,atomic propositions may yield different Boolean values at repeated…
The lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend lambda-PRK to…
We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be…
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an…
We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a…
The definition is a common form of human expert knowledge, a building block of formal science and mathematics, a foundation for database theory and is supported in various forms in many knowledge representation and formal specification…
In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. In addition, they enjoy a top-down symmetry and some…
We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue that these connectives model the information-erasure, the non-reversibility, and…
Type-free systems of logic are designed to consistently handle significant instances of self-reference. Some consistent type-free systems also have the feature of allowing the sort of general abstraction or comprehension principle that…
Relational parametricity was first introduced by Reynolds for System F. Although System F provides a strong model for the type systems at the core of modern functional programming languages, it lacks features of daily programming practice…
We define a fragment of monadic infinitary second-order logic corresponding to an abstract separation property. We use this to define the concept of a separation subclass. We use model theoretic techniques and games to show that separation…
We present a semantics based framework for analysing the quantitative behaviour of programs with regard to resource usage. We start from an operational semantics equipped with costs. The dioid structure of the set of costs allows for…
Free theorems are a popular tool in reasoning about parametrically polymorphic code. They are also of instructive use in teaching. Their derivation, though, can be tedious, as it involves unfolding a lot of definitions, then hoping to be…
We accommodate the Integrated Connectionist/Symbolic Architecture (ICS) of [32] within the categorical compositional semantics (CatCo) of [13], forming a model of categorical compositional cognition (CatCog). This resolves intrinsic…
Motivated by a recent conjecture concerning the expressiveness of declarative networking, we propose a formal computation model for "eventually consistent" distributed querying, based on relational transducers. A tight link has been…