Latest in cs.lo

total 10322took 0.12s
Generic derivations on o-minimal structuresMay 17 2019Let $T$ be a complete, model complete o-minimal theory extending the theory RCF of real closed ordered fields in some appropriate language $L$. We study derivations $\delta$ on models $\mathcal{M}\models T$. We introduce the notion of a $T$-derivation: ... More
Bisimulation Invariant Monadic-Second Order Logic in the FiniteMay 16 2019We consider bisimulation-invariant monadic second-order logic over various classes of finite transition systems. We present several combinatorial characterisations of when the expressive power of this fragment coincides with that of the modal mu-calculus. ... More
Reasoning about Cognitive Trust in Stochastic Multiagent SystemsMay 16 2019We consider the setting of stochastic multiagent systems modelled as stochastic multiplayer games and formulate an automated verification framework for quantifying and reasoning about agents' trust. To capture human trust, we work with a cognitive notion ... More
Effects Without Monads: Non-determinism -- Back to the Meta LanguageMay 16 2019We reflect on programming with complicated effects, recalling an undeservingly forgotten alternative to monadic programming and checking to see how well it can actually work in modern functional languages. We adopt and argue the position of factoring ... More
Mechanised Assurance Cases with Integrated Formal Methods in IsabelleMay 15 2019Assurance cases are often required as a means to certify a critical system. Use of formal methods in assurance can improve automation, and overcome problems with ambiguity, faulty reasoning, and inadequate evidentiary support. However, assurance cases ... More
A Non-wellfounded, Labelled Proof System for Propositional Dynamic LogicMay 15 2019We define a infinitary labelled sequent calculus for PDL, G3PDL^{\infty}. A finitarily representable cyclic system, G3PDL^{\omega}, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^{\infty} ... More
holpy: Interactive Theorem Proving in PythonMay 15 2019The design of modern proof assistants is faced with several sometimes conflicting goals, including scalability, extensibility, and soundness of proof checking. In this paper, we propose a new design for proof assistants, in an attempt to address some ... More
Quantitative Logic ReasoningMay 14 2019In this paper we show several similarities among logic systems that deal simultaneously with deductive and quantitative inference. We claim it is appropriate to call the tasks those systems perform as Quantitative Logic Reasoning. Analogous properties ... More
Enriched Lawvere Theories for Operational SemanticsMay 14 2019Enriched Lawvere theories are a generalization of Lawvere theories that allow us to describe the operational semantics of formal systems. For example, a graph-enriched Lawvere theory describes structures that have a graph of operations of each arity, ... More
Generic Encodings of Constructor Rewriting SystemsMay 14 2019Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages, with the negation ... More
Weighted parametric systems: Modelling and architecture specificationMay 14 2019Modern systems' design usually lies in multiple components which are connected via their interfaces. Synchronous applications, like IoT, require parametric systems, i.e., systems that aim to operate independently of the number of their components. A key ... More
Vaught's Conjecture for Almost Chainable TheoriesMay 14 2019A structure ${\mathbb Y}$ of a relational language $L$ is called almost chainable iff there are a finite set $F \subset Y$ and a linear order $<$ on the set $Y\setminus F$ such that for each partial automorphism $\varphi$ (i.e., local automorphism, in ... More
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTPMay 14 2019The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified ... More
Transtemporal edges and crosslayer edges in incompressible high-order networksMay 13 2019This work presents some outcomes of a theoretical investigation of incompressible high-order networks defined by a generalized graph representation. We study some of their network topological properties and how these may be related to real-world complex ... More
Operational semantics and program verification using many-sorted hybrid modal logicMay 13 2019We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which ... More
Finite burden in multivalued algebraically closed fieldsMay 13 2019We prove that an expansion of an algebraically closed field by $n$ arbitrary valuation rings is NTP${}_2$, and in fact has finite burden. It fails to be NIP, however, unless the valuation rings form a chain. Moreover, the incomplete theory of algebraically ... More
Quantifier Localization for DQBFMay 12 2019Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various ... More
Sequent-Type Proof Systems for Three-Valued Default LogicMay 12 2019Sequent-type proof systems constitute an important and widely-used class of calculi well-suited for analysing proof search. In my master's thesis, I introduce sequent-type calculi for a variant of default logic employing \Lukasiewicz's three-valued logic ... More
Rough Contact in General Rough MereologyMay 12 2019Theories of rough mereology have originated from diverse semantic considerations from contexts relating to study of databases, to human reasoning. These ideas of origin, especially in the latter context, are intensely complex. In this research, concepts ... More
Quantifying information flow in interactive systemsMay 10 2019We consider the problem of quantifying information flow in interactive systems, modelled as finite-state transducers in the style of Goguen and Meseguer. Our main result is that if the system is deterministic then the information flow is either logarithmic ... More
Horn Clauses in Hybrid-Dynamic First-Order LogicMay 10 2019We propose a hybrid-dynamic first-order logic as a formal foundation for specifying and reasoning about reconfigurable systems. As the name suggests, the formalism we develop extends (many-sorted) first-order logic with features that are common to hybrid ... More
Nets and Reverse Mathematics, a pilot studyMay 10 2019Nets are generalisations of sequences involving possibly uncountable index sets; this notion was introduced about a century ago by Moore and Smith. They also established the generalisation to nets of various basic theorems of analysis due to Bolzano-Weierstrass, ... More
Bidding Mechanisms in Graph GamesMay 09 2019In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner or payoff of the game. We study {\em bidding games} in which the players bid for the right to move the token. Several bidding ... More
On the Expressivity and Applicability of Model Representation FormalismsMay 09 2019A number of first-order calculi employ an explicit model representation formalism for automated reasoning and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of monadic, shallow, ... More
Determinacy in Discrete-Bidding Infinite-Duration GamesMay 09 2019In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and ... More
Strong completeness of modal logics over 0-dimensional metric spacesMay 09 2019We prove strong completeness results for some modal logics with the universal modality, with respect to their topological semantics over 0-dimensional dense-in-themselves metric spaces. We also use failure of compactness to show that, for some languages ... More
SMT-based Constraint Answer Set Solver EZSMT+May 08 2019Constraint answer set programming integrates answer set programming with constraint processing. System EZSMT+ is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search. Its theoretical foundation lies on ... More
Discovering and Proving Invariants in Answer Set Programming and PlanningMay 08 2019Answer set programming (ASP) and planning are two widely used paradigms for solving logic programs with declarative programming. In both cases, the quality of the input programs has a major influence on the quality and performance of the solving or planning ... More
On Church's Thesis in Cubical AssembliesMay 08 2019We show that Church's thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show that nevertheless Church's thesis is consistent with univalent type theory ... More
Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithmMay 08 2019May 09 2019We show that the 2-dimensional Weisfeiler-Leman algorithm stabilizes n-vertex graphs after at most O(n log n) iterations. This implies that if such graphs are distinguishable in 3-variable first order logic with counting, then they can also be distinguished ... More
Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithmhttps://arxiv.org/submit/2681062/previewMay 08 2019We show that the 2-dimensional Weisfeiler-Leman algorithm stabilizes n-vertex graphs after at most O(n log n) iterations. This implies that if such graphs are distinguishable in 3-variable first order logic with counting, then they can also be distinguished ... More
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point NumbersMay 07 2019Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or pseudo-Boolean terms. However, many SMT and OMT applications, in ... More
A SAT-based System for Consistent Query AnsweringMay 07 2019An inconsistent database is a database that violates one or more integrity constraints, such as functional dependencies. Consistent Query Answering is a rigorous and principled approach to the semantics of queries posed against inconsistent databases. ... More
A Type Theory for Defining Logics and ProofsMay 07 2019We describe a Martin-L\"of-style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) ... More
Integrated Algorithms for HEX-Programs and Applications in Machine LearningMay 07 2019This paper summarizes my doctoral research on evaluation algorithms for HEX-programs, which extend Answer Set Programming with means for interfacing external computations. The focus is on integrating different subprocesses of HEX-evaluation, such as solving ... More
Design Space Exploration via Answer Set Programming Modulo TheoriesMay 07 2019The design of embedded systems, that are ubiquitously used in mobile devices and cars, is becoming continuously more complex such that efficient system-level design methods are becoming crucial. My research aims at developing systems that help the designer ... More
Design Space Exploration as Quantified SatisfactionMay 07 2019We propose novel algorithms for design and design space exploration. The designs computed by these algorithms are compositions of function types specified in component libraries. Our algorithms reduce the design problem to quantified satisfiability and ... More
Selection properties of the split interval and the Continuum HypothesisMay 06 2019We prove that every usco multimap $\Phi:X\to Y$ from a metrizable separable space $X$ to a GO-space $Y$ has an $F_\sigma$-measurable selection. On the other hand, for the split interval $\ddot{\mathbb I}$ and the projection $P:\ddot{\mathbb I}^2\to{\mathbb ... More
Revisiting Counter-model Generation for Minimal Implicational LogicMay 06 2019The $\mathbf{LMT^{\rightarrow}}$ sequent calculus was introduced in Santos (2016). This paper presents a Termination proof and a new (more direct) Completeness proof for it. $\mathbf{LMT^{\rightarrow}}$ is aimed to be used for proof search in Propositional ... More
Revisiting Counter-model Generation for Minimal Implicational LogicMay 06 2019May 07 2019The $\mathbf{LMT^{\rightarrow}}$ sequent calculus was introduced in 2016 by the same authors. This paper presents a Termination proof and a new (more direct) Completeness proof for it. $\mathbf{LMT^{\rightarrow}}$ is aimed to be used for proof search ... More
Interaction with Formal Mathematical Documents in Isabelle/PIDEMay 05 2019Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized mathematics in Isabelle/HOL. ... More
Answer Set Solving exploiting Treewidth and its LimitsMay 05 2019Parameterized algorithms have been subject to extensive research of recent years and allow to solve hard problems by exploiting a parameter of the corresponding problem instances. There, one goal is to devise algorithms, where the runtime is exponential ... More
A Typedriven Vector Semantics for Ellipsis with Anaphora using Lambek Calculus with Limited ContractionMay 05 2019We develop a vector space semantics for verb phrase ellipsis with anaphora using type-driven compositional distributional semantics based on the Lambek calculus with limited contraction (LCC) of J\"ager (2006). Distributional semantics has a lot to say ... More
A reconstruction of the multipreference closureMay 05 2019The paper describes a preferential approach for dealing with exceptions in KLM preferential logics, based on the rational closure. It is well known that the rational closure does not allow an independent handling of the inheritance of different defeasible ... More
Learning families of algebraic structures from informantMay 05 2019We combine computable structure theory and algorithmic learning theory to study learning of families of algebraic structures. Our main result is a model-theoretic characterization of the class $\mathbf{InfEx}_{\cong}$, consisting of the structures whose ... More
Nilpotent Group-Counterexamples to Zilbers ConjectureMay 05 2019We construct uncountably categorical 3-nilpotent groups of exponent p > 3. They are not one-based and do not allow the interpretation of an infinite field. Therefore they are counterexamples to Zilbers Conjecture. First 2-nilpotent new uncoutably categorical ... More
A Logic Framework for P2P Deductive DatabasesMay 04 2019This paper presents a logic framework for modeling the interaction among deductive databases in a P2P (Peer to Peer) environment. Each peer joining a P2P system provides or imports data from its neighbors by using a set of mapping rules, i.e. a set of ... More
A categorical construction for the computational definition of vector spacesMay 04 2019Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type ... More
Compactness of first-order fuzzy logicsMay 04 2019One of the nice properties of the first-order logic is the compactness of satisfiability. It state that a finitely satisfiable theory is satisfiable. However, different degrees of satisfiability in many-valued logics, poses various kind of the compactness ... More
Game Semantics of Martin-Löf Type TheoryMay 03 2019We present game semantics of Martin-L\"of type theory (MLTT), which solves a long-standing problem open for more than twenty years. More specifically, we introduce a category with families of a novel variant of games, which induces an interpretation of ... More
Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent SystemsMay 02 2019We develop a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems (HDMAS). Homogeneity means that all agents have the same available actions at any given state ... More
From Specifications to Behavior: Maneuver Verification in a Semantic State SpaceMay 02 2019To realize a market entry of autonomous vehicles in the foreseeable future, the behavior planning system will need to abide by the same rules that humans follow. Product liability cannot be enforced without a proper solution to the approval trap. In this ... More
Convex choice, finite choice and sortingMay 02 2019We study the Weihrauch degrees of closed choice for finite sets, closed choice for convex sets and sorting infinite sequences over finite alphabets. Our main results are: One, that choice for finite sets of cardinality $i + 1$ is reducible to choice for ... More
Discrete time stochastic and deterministic Petri box calculusMay 01 2019We propose an extension with deterministically timed multiactions of discrete time stochastic and immediate Petri box calculus (dtsiPBC), previously presented by I.V. Tarasyuk, H. Maci\`a and V. Valero. In dtsdPBC, non-negative integers specify multiactions ... More
Computer Science and Metaphysics: A Cross-FertilizationMay 01 2019Computational philosophy is the use of mechanized computational techniques to unearth philosophical insights that are either difficult or impossible to find using traditional philosophical methods. Computational metaphysics is computational philosophy ... More
QKD in Isabelle -- Bayesian CalculationMay 01 2019In this paper, we present a first step towards a formalisation of the Quantum Key Distribution algorithm in Isabelle. We focus on the formalisation of the main probabilistic argument why Bob cannot be certain about the key bit sent by Alice before he ... More
The Sierpinski Object in the Scott Realizability ToposApr 30 2019We study the Sierpinski Object in the Scott Realizability Topos.
Behavioral Program Logic and LAGC Semantics without Continuations (Technical Report)Apr 30 2019We present Behavioral Program Logic (BPL), a dynamic logic for trace properties that incorporates concepts from behavioral types and allows reasoning about non-functional properties within a sequent calculus. BPL uses behavioral modalities [s |- {\tau} ... More
Overlap Algebras: a constructive look at complete Boolean algebrasApr 30 2019The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although classically equivalent ... More
Quantitative continuity and computable analysis in CoqApr 30 2019We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable ... More
Semantic Referee: A Neural-Symbolic Framework for Enhancing Geospatial Semantic SegmentationApr 30 2019Understanding why machine learning algorithms may fail is usually the task of the human expert that uses domain knowledge and contextual information to discover systematic shortcomings in either the data or the algorithm. In this paper, we propose a semantic ... More
On the incomputability of computable dimensionApr 30 2019Using an iterative tree construction we show that for simple computable subsets of the Cantor space Hausdorff, constructive and computable dimensions amight be incomputable.
QRATPre+: Effective QBF Preprocessing via Strong Redundancy PropertiesApr 29 2019We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong redundancy properties of clauses and universal literals. QRATPre+ is the ... More
QRATPre+: Effective QBF Preprocessing via Strong Redundancy PropertiesApr 29 2019May 06 2019We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong redundancy properties of clauses and universal literals. QRATPre+ is the ... More
Tracelets and Tracelet Analysis Of Compositional Rewriting SystemsApr 29 2019Taking advantage of a recently discovered associativity property of rule compositions, we extend the classical concurrency theory for rewriting systems over adhesive categories. We introduce the notion of tracelets, which are defined as minimal derivation ... More
A Complete Classification of the Complexity and Rewritability of Ontology-Mediated Queries based on the Description Logic ELApr 29 2019We provide an ultimately fine-grained analysis of the data complexity and rewritability of ontology-mediated queries (OMQs) based on an EL ontology and a conjunctive query (CQ). Our main results are that every such OMQ is in AC0, NL-complete, or PTime-complete ... More
Model Theory, Arithmetic & Algebraic GeometryApr 28 2019In this pages I give an overview of the relationship between Model Theory, Arithmetic and Algebraic Geometry. The topics will be the basic ones in the area, so this is just an invitation, in the presentation of topics I mainly follow the philosophy of ... More
Parameterised Counting Classes with Bounded NondeterminismApr 27 2019Stockhusen and Tantau (IPEC 2013) introduced the operators paraW and paraBeta for parameterised space complexity classes by allowing bounded nondeterminism with read-only and read-once access, respectively. Using these operators, they could characterise ... More
Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)Apr 27 2019We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential ... More
The Category of Node-and-Choice Forms, with Subcategories for Choice-Sequence Forms and Choice-Set FormsApr 27 2019The literature specifies extensive-form games in many styles, and eventually I hope to formally translate games across those styles. Toward that end, this paper defines $\mathbf{NCF}$, the category of node-and-choice forms. The category's objects are ... More
Graph Neural Reasoning for 2-Quantified Boolean Formula SolversApr 27 2019In this paper, we investigate the feasibility of learning GNN (Graph Neural Network) based solvers and GNN-based heuristics for specified QBF (Quantified Boolean Formula) problems. We design and evaluate several GNN architectures for 2QBF formulae, and ... More
A certifying extraction with time bounds from Coq to call-by-value $λ$-calculusApr 26 2019We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value $\lambda$-calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify ... More
Quantitative Logics for Equivalence of Effectful ProgramsApr 26 2019In order to reason about effects, we can define quantitative formulas to describe behavioural aspects of effectful programs. These formulas can for example express probabilities that (or sets of correct starting states for which) a program satisfies a ... More
Reward-Based Deception with Cognitive BiasApr 25 2019Deception plays a key role in adversarial or strategic interactions for the purpose of self-defence and survival. This paper introduces a general framework and solution to address deception. Most existing approaches for deception consider obfuscating ... More
Interpolation and the Array Property FragmentApr 25 2019Interpolation based software model checkers have been successfully employed to automatically prove programs correct. Their power comes from interpolating SMT solvers that check the feasibility of potential counterexamples and compute candidate invariants, ... More
Accessible categories, set theory, and model theory: an invitationApr 25 2019We give a self-contained introduction to accessible categories and how they shed light on both model- and set-theoretic questions. We survey for example recent developments on the study of presentability ranks, a notion of cardinality localized to a given ... More
The game semantics of game theoryApr 25 2019We use a reformulation of compositional game theory to reunite game theory with game semantics, by viewing an open game as the System and its choice of contexts as the Environment. Specifically, the system is jointly controlled by $n \geq 0$ noncooperative ... More
Deductive Proof of Ethereum Smart Contracts Using Why3Apr 25 2019A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used ... More
On Learning to ProveApr 24 2019Apr 26 2019In this paper, we consider the problem of learning a (first-order) theorem prover where we use a representation of beliefs in mathematical claims instead of a proof system to search for proofs. The inspiration for doing so comes from the practices of ... More
On Learning to ProveApr 24 2019In this paper, we consider the problem of learning a (first-order) theorem prover where we use a representation of beliefs in mathematical claims instead of a proof system to search for proofs. The inspiration for doing so comes from the practices of ... More
The Ideal Approach to Computing Closed Subsets in Well-Quasi-OrderingApr 24 2019Elegant and general algorithms for handling upwards-closed and downwards-closed subsets of WQOs can be developed using the filter-based and ideal-based representation for these sets. These algorithms can be built in a generic or parameterized way, in ... More
Circuit Relations for Real Stabilizers: Towards TOF+HApr 24 2019The real stabilizer fragment of quantum mechanics was shown to have a complete axiomatization in terms of the angle-free fragment of the ZX-calculus. This fragment of the ZXcalculus--although abstractly elegant--is stated in terms of identities, such ... More
The differential calculus of causal functionsApr 24 2019Causal functions of sequences occur throughout computer science, from theory to hardware to machine learning. Mealy machines, synchronous digital circuits, signal flow graphs, and recurrent neural networks all have behaviour that can be described by causal ... More
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4Apr 24 2019We propose a "modal linear logic" to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, ... More
A formalization of forcing and the unprovability of the continuum hypothesisApr 23 2019We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, ... More
Some Problems in Logic: Applications of Kripke's Notion of FulfilmentApr 23 2019This is a study of S. Kripke's notion of fulfilment. Motivated by Paris-Harrington statement, Kripke was looking for a proof of G\"odel's Incompleteness Theorem which was model-theoretic, natural (without self-reference), and easy. Fulfilment gives a ... More
The Theorem Prover Museum -- Conserving the System Heritage of Automated ReasoningApr 23 2019We present the Theorem Prover Museum, and initiative to conserve -- and make publicly available -- the sources and source-related artefacts of automated reasoning systems. Theorem provers have been at the forefront of Artificial Intelligence, stretching ... More
On uniform definability of types over finite sets for NIP formulasApr 23 2019Combining two results from machine learning theory we prove that a formula is NIP if and only if it satisfies uniform definability of types over finite sets (UDTFS). This settles a conjecture of Laskowski.
The birth of the contradictory component in random 2-SATApr 23 2019We prove that, with high probability, the contradictory components of a random 2-SAT formula in the subcritical phase of the phase transition have only 3-regular kernels. This follows from the relation between these kernels and the complex component of ... More
Two variable fragment of Term Modal LogicApr 23 2019Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$. Like First order modal logic, ... More
Two variable fragment of Term Modal LogicApr 23 2019Apr 27 2019Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$. Like First order modal logic, ... More
Bounds in Query LearningApr 23 2019We introduce new combinatorial quantities for concept classes, and prove lower and upper bounds for learning complexity in several models of query learning in terms of various combinatorial quantities. Our approach is flexible and powerful enough to enough ... More
A Category Theoretic Interpretation of Gandy's Principles for MechanismsApr 23 2019Based on Gandy's principles for models of computation we give category-theoretic axioms describing locally deterministic updates to finite objects. Rather than fixing a particular category of states, we describe what properties such a category should ... More
Intersection Subtyping with ConstructorsApr 23 2019We study the question of extending the BCD intersection type system with additional type constructors. On the typing side, we focus on adding the usual rules for product types. On the subtyping side, we consider a generic way of defining a subtyping relation ... More
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-CalculusApr 23 2019We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value lambda-calculus. For this purpose, we use ... More
Natural Deduction and Normalization Proofs for the Intersection Type DisciplineApr 23 2019Refining and extending previous work by Retor\'e, we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in parallel. ... More
Intersection Types for Unboundedness ProblemsApr 23 2019Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing ... More
A comonadic view of simulation and quantum resourcesApr 22 2019We study simulation and quantum resources in the setting of the sheaf-theoretic approach to contextuality and non-locality. Resources are viewed behaviourally, as empirical models. In earlier work, a notion of morphism for these empirical models was proposed ... More
A note on the effective listing of complete typesApr 22 2019We use the "geometric axioms" point of view to give an effective listing of the complete types of the theory $DCF_{0}$ of differentially closed fields of characteristic $0$. This gives another account of observations made in earlier papers.
Strand Spaces with Choice via a Process Algebra SemanticsApr 22 2019Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic ... More