相关论文: Linear Abadi and Plotkin Logic

In functional programming, datatypes a la carte provide a convenient modular representation of recursive datatypes, based on their initial algebra semantics. Unfortunately it is highly challenging to implement this technique in proof…

Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type {\Omega}, the auto- autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most…

Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic…

A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanized using Isabelle. Least fixedpoints express inductive data types such as strict lists; greatest fixedpoints express coinductive…

We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational…

We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions and iterated connectives ranging over intervals parameterized by arithmetic variables. The satisfiability problem is shown…

Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality $!_r$ captures how many times a…

This paper presents a plausible reasoning system to illustrate some broad issues in knowledge representation: dualities between different reasoning forms, the difficulty of unifying complementary reasoning styles, and the approximate nature…

The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new operations, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new…

Stereotypical reasoning assumes that the situation at hand is one of a kind and that it enjoys the properties generally associated with that kind of situation. It is one of the most basic forms of nonmonotonic reasoning. A formal model for…

We develop a second-order extension of intuitionistic modal logic, allowing quantification over propositions, both syntactically and semantically. A key feature of second-order logic is its capacity to define positive connectives from the…

Reasoning with quantifier expressions in natural language combines logical and arithmetical features, transcending strict divides between qualitative and quantitative. Our topic is this cooperation of styles as it occurs in common…

In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in…

We explore end-to-end trained differentiable models that integrate natural logic with neural networks, aiming to keep the backbone of natural language reasoning based on the natural logic formalism while introducing subsymbolic vector…

We prove completeness, interpolation, decidability and an omitting types theorem for certain multi dimensional modal logics where the states are not abstract entities but have an inner structure. The states will be sequences. Our approach…

This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…

The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural…

We construct a symmetric monoidal closed category of polynomial endofunctors (as objects) and simulation cells (as morphisms). This structure is defined using universal properties without reference to representing polynomial diagrams and is…

We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system…

In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard…