Latest in cs.lo

total 7325took 0.20s
A Separation Logic for Concurrent Randomized ProgramsFeb 08 2018We present a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic ... More
Classical Higher-Order ProcessesFeb 08 2018Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between session types ... More
Impredicative Encodings of (Higher) Inductive TypesFeb 08 2018Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To recover {\eta} ... More
Stubborn Transaction Reduction (with Proofs)Feb 08 2018The exponential explosion of parallel interleavings remains a fundamental challenge to model checking of concurrent programs. Both partial-order reduction (POR) and transaction reduction (TR) decrease the number of interleavings in a concurrent system. ... More
Definable Ellipsoid Method, Sums-of-Squares Proofs, and the Isomorphism ProblemFeb 07 2018The ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method for showing that this reduction ... More
A Schematic Definition of Quantum Polynomial Time ComputabilityFeb 07 2018In the past four decades, the notion of quantum polynomial-time computability has been realized by the theoretical models of quantum Turing machines and quantum circuits. Here, we seek a third model, which is a quantum analogue of the schematic (inductive ... More
Neighborhood Contingency Logic: A New PerspectiveFeb 07 2018In this paper, we propose a new neighborhood semantics for contingency logic, by introducing a simple property in standard neighborhood models. This simplifies the neighborhood semantics given in (Fan and van Ditmarsch, 2015), but does not change the ... More
Cellular Cohomology in Homotopy Type TheoryFeb 06 2018We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many ... More
Deciding Detectability for Labeled Petri NetsFeb 06 2018Detectability of discrete event systems (DESs) is a property to determine a priori whether the current and subsequent states can be determined based on observations. In this paper, we investigate the verification of two detectability properties -- strong ... More
Büchi-Kamp Theorems for 1-clock ATAFeb 06 2018This paper investigates Kamp-like and B\"uchi-like theorems for 1-clock Alternating Timed Automata (1-ATA) and its natural subclasses. A notion of 1-ATA with loop-free-resets is defined. This automaton class is shown to be expressively equivalent to the ... More
Programming infinite machinesFeb 06 2018For infinite machines which are free from the classical Thompson's lamp paradox we show that they are not free from its inverted version. We provide a program for infinite machines and an infinite mechanism which simulate this paradox. While their finite ... More
Causal Linearizability: Compositionality for Partially Ordered ExecutionsFeb 06 2018In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only ... More
Tight Bounds on the Asymptotic Descriptive Complexity of Subgraph IsomorphismFeb 06 2018Let $v(F)$ denote the number of vertices in a fixed connected pattern graph $F$. We show an infinite family of patterns $F$ such that the existence of a subgraph isomorphic to $F$ is expressible by a first-order sentence of quantifier depth $\frac23\,v(F)+1$, ... More
Reducing CMSO Model Checking to Highly Connected GraphsFeb 05 2018Given a Counting Monadic Second Order (CMSO) sentence $\psi$, the CMSO$[\psi]$ problem is defined as follows. The input to CMSO$[\psi]$ is a graph $G$, and the objective is to determine whether $G\models \psi$. Our main theorem states that for every CMSO ... More
Verifying Asymptotic Time Complexity of Imperative Programs in IsabelleFeb 05 2018We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include running time. In addition to the basic arguments, our framework is able ... More
On Higher Inductive Types in Cubical Type TheoryFeb 04 2018Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in ... More
Parametric Presburger Arithmetic: Complexity of Counting and Quantifier EliminationFeb 03 2018We consider an expansion of Presburger arithmetic which allows multiplication by $k$ parameters $t_1,\ldots,t_k$. A formula in this language defines a parametric set $S_\mathbf{t} \subseteq \mathbb{Z}^{d}$ as $\mathbf{t}$ varies in $\mathbb{Z}^k$, and ... More
Disjunctive Axioms and Concurrent $λ$-Calculi: a Curry-Howard ApproachFeb 03 2018We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $\lambda$-calculi; each of them features a specific communication mechanism, including broadcasting and ... More
HOL Light QEFeb 01 2018We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax. ${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes ... More
On the computability of graphonsJan 31 2018We investigate the relative computability of exchangeable binary relational data when presented in terms of the distribution of an invariant measure on graphs, or as a graphon in either $L^1$ or the cut distance. We establish basic computable equivalences, ... More
Dugundji systems and a retract characterization of effective zero-dimensionalityJan 31 2018In a previous paper, the author considered several conditions for effective zero-dimensionality of a computable metric space $X$; each of the (classically equivalent) properties of having vanishing small or large inductive dimension, or covering dimension, ... More
Indistinguishable binomial decision tree of 3-SAT: Proof of class P is a proper subset of class NPJan 30 2018This paper solves a long standing open problem of whether NP-complete problems could be solved in polynomial time on a deterministic Turing machine by showing that the indistinguishable binomial decision tree can be formed in a 3-SAT instance. This paper ... More
Logic characterisation of p/q-recognisable setsJan 26 2018Let $\frac{p}{q}$ be a rational number. Numeration in base $\frac{p}{q}$ is defined by a function that evaluates each finite word over $A_p=\{0,1,\ldots,{p-1}\}$ to a rational number in some set $N_{\frac{p}{q}}$. In particular, $N_{\frac{p}{q}}$ contains ... More
Reasoning about effects: from lists to cyber-physical agentsJan 24 2018Theories for reasoning about programs with effects initially focused on basic manipulation of lists and other mutable data. The next challenge was to consider higher-order programming, adding functions as first class objects to mutable data. Reasoning ... More
Internal Universes in Models of Homotopy Type TheoryJan 23 2018Jan 26 2018We show that universes of fibrations in various models of homotopy type theory have an essentially global character: they cannot be described in the internal language of the presheaf topos from which the model is constructed. We get around this problem ... More
Type-two polynomial-time and restricted lookaheadJan 23 2018This paper provides an alternate characterization of type-two polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In contrast ... More
Higher-Order Equational Pattern Anti-Unification [Preprint]Jan 23 2018We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order ... More
Some model theory for the modal $μ$-calculus: syntactic characterisations of semantic propertiesJan 18 2018Feb 05 2018This paper contributes to the theory of the modal $\mu$-calculus by proving some model-theoretic results. More in particular, we discuss a number of semantic properties pertaining to formulas of the modal $\mu$-calculus. For each of these properties we ... More
Complexity of Combinations of Qualitative Constraint Satisfaction ProblemsJan 18 2018The CSP of a first-order theory $T$ is the problem of deciding for a given finite set $S$ of atomic formulas whether $T \cup S$ is satisfiable. Let $T_1$ and $T_2$ be two theories with countably infinite models and disjoint signatures. Nelson and Oppen ... More
Supersimple omega-categorical theories and pregeometriesJan 17 2018We prove that if $T$ is an $\omega$-categorical supersimple theory with nontrivial dependence (given by dividing/forking), then there is a nontrivial regular 1-type over a finite set of reals which is realized by real elements; hence dividing induces ... More
Finitary-based Domain Theory in Coq: An Early ReportJan 17 2018In domain theory every finite computable object can be represented by a single mathematical object instead of a set of objects, using the notion of finitary-basis. In this article we report on our effort to formalize domain theory in Coq in terms of finitary-basis. ... More
Markings in Perpetual Free-Choice Nets Are Fully Characterized by Their Enabled TransitionsJan 12 2018A marked Petri net is lucent if there are no two different reachable markings enabling the same set of transitions, i.e., states are fully characterized by the transitions they enable. This paper explores the class of marked Petri nets that are lucent ... More
On singularity properties of convolutions of algebraic morphismsJan 09 2018Let $K$ be a field of characteristic zero, $X$ and $Y$ be smooth $K$-varieties, and let $V$ be a finite dimensional $K$-vector space. For two algebraic morphisms $\varphi:X\rightarrow V$ and $\psi:Y\rightarrow V$ we define a convolution operation, $\varphi*\psi:X\times ... More
Towards platform-independent verification of the standard mathematical functions: the square root functionJan 03 2018Jan 25 2018The paper presents (human-oriented) specification and (pen-and-paper) verification of the square root function. The function implements Newton method and uses a look-up table for initial approximations. Specification is done in terms of total correctness ... More
Unifying Theories of Reactive Design ContractsDec 29 2017Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions and guarantees of each component. In this paper, we describe a unifying ... More
Unifying Theories of Timed with Generalised Reactive ProcessesDec 29 2017Hoare and He's theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. ... More
Profiniteness in finitely generated varieties is undecidableDec 25 2017Profinite algebras are exactly those that are isomorphic to inverse limits of finite algebras. Such algebras are naturally equipped with Boolean topologies. A variety $\mathcal V$ is standard if every Boolean topological algebra with the algebraic reduct ... More
The Algebraic View of ComputationDec 09 2017We argue that computation is an abstract algebraic concept, and a computer is a result of a morphism (a structure preserving map) from a finite universal semigroup.
Alignment-based Translations Across Formal Systems Using Interface TheoriesDec 05 2017Translating expressions between different logics and theorem provers is notoriously and often prohibitively difficult, due to the large differences between the logical foundations, the implementations of the systems, and the structure of the respective ... More
Language and Proofs for Higher-Order SMT (Work in Progress)Dec 05 2017Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. ... More
Synthesizing Functional Reactive ProgramsDec 01 2017We present the first method to synthesize functional reactive programs from temporal logic specifications. Existing algorithms for the synthesis of reactive systems target finite-state implementations, such as hardware circuits, but fail when it comes ... More
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & ResultsNov 29 2017We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe the benchmark selection, evaluation scheme and the experimental setup of ... More
Symbolic vs. Bounded Synthesis for Petri GamesNov 29 2017Petri games are a multiplayer game model for the automatic synthesis of distributed systems. We compare two fundamentally different approaches for solving Petri games. The symbolic approach decides the existence of a winning strategy via a reduction to ... More
XSAT of Linear CNF FormulasNov 20 2017Jan 18 2018Open questions with respect to the computational complexity of linear CNF formulas in connection with regularity and uniformity are addressed. In particular it is proven that any l-regular monotone CNF formula is XSAT-unsatisfiable if its number of clauses ... More
Real-time Stream-based MonitoringNov 10 2017We introduce RTLola, a new stream-based specification language for the description of real-time properties of reactive systems. In real-time applications, data arrives at varying rates and in most cases it is hard to predict the input rate. The integration ... More
The univalence axiom in cubical setsOct 30 2017In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model ... More
Permissive Finite-State Controllers of POMDPs using Parameter SynthesisOct 24 2017We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs). The key insight is that computing (randomized) FSCs on POMDPs is equivalent to synthesis for parametric Markov chains (pMCs). This correspondence enables ... More
Ranking Functions for Vector Addition SystemsOct 23 2017Vector addition systems are an important model in theoretical computer science and have been used for the analysis of systems in a variety of areas. Termination is a crucial property of vector addition systems and has received considerable interest in ... More
Privacy by typing in the $π$-calculusOct 17 2017Dec 17 2017In this paper we propose a formal framework for studying privacy in information systems. The proposal follows a two-axes schema where the first axis considers privacy as a taxonomy of rights and the second axis involves the ways an information system ... More
Symmetric SynthesisOct 16 2017We study the problem of determining whether a given temporal specification can be implemented by a symmetric system, i.e., a system composed from identical components. Symmetry is an important goal in the design of distributed systems, because systems ... More
Synthesis in Distributed EnvironmentsOct 15 2017Most approaches to the synthesis of reactive systems study the problem in terms of a two-player game with complete observation. In many applications, however, the system's environment consists of several distinct entities, and the system must actively ... More
Causality-based Model CheckingOct 10 2017Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of ... More
Stone-Type Dualities for Separation LogicsOct 09 2017Stone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because they strengthen soundness and completeness to a categorical equivalence, yielding a framework through which both algebraic and ... More
Towards a Minimal Stabilizer ZX-calculusSep 26 2017The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one if and only if these two diagrams represent the same quantum ... More
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained ReachabilitySep 07 2017Since the introduction of Alternating-time Temporal Logic (ATL), many logics have been proposed to reason about different strategic capabilities of the agents of a system. In particular, some logics have been designed to reason about the uniform memoryless ... More
Model Checking Social Network ModelsSep 07 2017A social network service is a platform to build social relations among people sharing similar interests and activities. The underlying structure of a social networks service is the social graph, where nodes represent users and the arcs represent the users' ... More
Automorphism groups of finite topological rankSep 06 2017We offer a criterion for showing that the automorphism group of an ultrahomogeneous structure is topologically 2-generated and even has a cyclically dense conjugacy class. We then show how finite topological rank of the automorphism group of an $\omega$-categorical ... More
Verifying Security Policies in Multi-agent Workflows with LoopsAug 29 2017We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number ... More
A Survey of Runtime Monitoring Instrumentation TechniquesAug 24 2017Runtime Monitoring is a lightweight and dynamic verification technique that involves observing the internal operations of a software system and/or its interactions with other external entities, with the aim of determining whether the system satisfies ... More
Timed Epistemic Knowledge Bases for Social Networks (Extended Version)Aug 14 2017Sep 08 2017We present an epistemic logic equipped with time-stamps in the atoms and epistemic operators, which allows to reason not only about information available to the different agents, but also about the moments at which events happens and new knowledge is ... More
A Verified Compiler for Probability Density FunctionsJul 21 2017Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple probabilistic functional language. In this work, we implement such a compiler for a modified version of this language ... More
Some NIP-like phenomena in NTP$_{2}$Jul 17 2017We introduce the notion of an NTP$_{2}$-smooth measure and prove that they exist assuming NTP$_{2}$. Using this, we propose a notion of distality in NTP$_{2}$ that unfortunately does not intersect simple theories trivially. We then prove a finite alternation ... More
A criterion for "easiness" of certain SAT problemsJul 01 2017A generalized 1-in-3SAT problem is defined and found to be in complexity class P when restricted to a certain subset of CNF expressions. In particular, 1-in-kSAT with no restrictions on the number of literals per clause can be decided in polynomial time ... More
Accurate and Efficient Profile Matching in Knowledge BasesJun 21 2017Nov 17 2017A profile describes a set of properties, e.g. a set of skills a person may have, a set of skills required for a particular job, or a set of abilities a football player may have with respect to a particular team strategy. Profile matching aims to determine ... More
Canonical Selection of ColimitsMay 25 2017Colimits are a powerful tool for the combination of objects in a category. In the context of modeling and specification, they are used in the institution-independent semantics (1) of instantiations of parameterised specifications (e.g. in the specification ... More
A complete characterisation of All-versus-Nothing arguments for stabiliser statesMay 23 2017An important class of contextuality arguments in quantum foundations are the All-versus-Nothing (AvN) proofs, generalising a construction originally due to Mermin. We present a general formulation of All-versus-Nothing arguments, and a complete characterisation ... More
Strategically knowing howMay 15 2017In this paper, we propose a single-agent logic of goal-directed knowing how extending the standard epistemic logic of knowing that with a new knowing how operator. The semantics of the new operator is based on the idea that knowing how to achieve $\phi$ ... More
Proceedings 14th International Workshop on the ACL2 Theorem Prover and its ApplicationsMay 02 2017This volume contains the proceedings of the Fourteenth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2017, a two-day workshop held in Austin, Texas, USA, on May 22-23, 2017. ACL2 workshops occur at approximately 18-month ... More
Polynomial time estimates for #SATMay 01 2017Limits on the number of satisfying assignments for CNS instances with n variables and m clauses are derived from various inequalities. Some bounds can be calculated in polynomial time, sharper bounds demand information about the distribution of the number ... More
Boundedness and absoluteness of some dynamical invariants in model theoryApr 29 2017Let ${\mathfrak C}$ be a monster model of an arbitrary theory $T$, $\bar \alpha$ any tuple of bounded length of elements of ${\mathfrak C}$, and $\bar c$ an enumeration of all elements of ${\mathfrak C}$. By $S_{\bar \alpha}({\mathfrak C})$ denote the ... More
A minimal representation for continuous functionsMar 29 2017This paper presents a variation of a celebrated result of Kawamura and Cook specifying the least set of information about a continuous function on the unit interval which is needed for fast function evaluation. To make the above description precise, one ... More
Transseries as germs of surreal functionsMar 06 2017Oct 05 2017We show that \'Ecalle's transseries and their variants (LE and EL-series) can be interpreted as functions from positive infinite surreal numbers to surreal numbers. The same holds for a much larger class of formal series, here called omega-series. Omega-series ... More
DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCLFeb 27 2017May 30 2017We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional ... More
Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all ModelsFeb 22 2017Apr 28 2017We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ... More
Intuitionistic Layered Graph Logic: Semantics and Proof TheoryFeb 19 2017Feb 27 2017Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic that gives an account ... More
Is your software on dope? Formal analysis of surreptitiously "enhanced" programsFeb 15 2017Usually, it is the software manufacturer who employs verification or testing to ensure that the software embedded in a device meets its main objectives. However, these days we are confronted with the situation that economical or technological reasons ... More
ZX-Calculus: Cyclotomic Supplementarity and Incompleteness for Clifford+T quantum mechanicsFeb 07 2017Jun 26 2017The ZX-Calculus is a powerful graphical language for quantum mechanics and quantum information processing. The completeness of the language -- i.e. the ability to derive any true equation -- is a crucial question. In the quest of a complete ZX-calculus, ... More
Y-Calculus: A language for real Matrices derived from the ZX-CalculusFeb 03 2017The ZX-Calculus is a powerful diagrammatic language devoted to represent complex quantum evolutions. But the advantages of quantum computing still exist when working with rebits, and evolutions with real coefficients. Some models explicitly use rebits, ... More
Two forms of minimality in ASPIC+Feb 02 2017Many systems of structured argumentation explicitly require that the facts and rules that make up the argument for a conclusion be the minimal set required to derive the conclusion. ASPIC+ does not place such a requirement on arguments, instead requiring ... More
Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword OrderingJan 25 2017We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $\Sigma_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering ... More
Evaluating QBF Solvers: Quantifier Alternations MatterJan 23 2017May 03 2017We present an experimental study of the effects of alternation bias in the evaluation of quantified Boolean formula (QBF) solvers. Alternation bias in a set of QBFs in prenex conjunctive normal form (PCNF) is caused by an overrepresentation of PCNFs with ... More
The complexity of quantified constraints using the algebraic formulationJan 15 2017Apr 27 2017Let A be an idempotent algebra on a finite domain. We combine results of Chen, Zhuk and Carvalho et al. to argue that if A satisfies the polynomially generated powers property (PGP), then QCSP(Inv(A)) is in NP. We then use the result of Zhuk to prove ... More
Bounded time computation on metric spaces and Banach spacesJan 09 2017Mar 29 2017We extend the framework by Kawamura and Cook for investigating computational complexity for operators occurring in analysis. This model is based on second-order complexity theory for functions on the Baire space, which is lifted to metric spaces by means ... More
An early sign of satisfiabilityDec 15 2016This note considers checking satisfiability of sets of propositional clauses (SAT instances). It shows that "unipolar sets" of clauses (containing no positive or no negative clauses) provide an "early sign" of satisfiability of SAT instances before all ... More
A Generalization of the Curry-Howard CorrespondenceDec 08 2016We present a variant of the calculus of deductive systems developed in (Lambek 1972, 1974), and give a generalization of the Curry-Howard-Lambek theorem giving an equivalence between the category of typed lambda-calculi and the category of cartesian closed ... More
Incorporating Quotation and Evaluation Into Church's Type TheoryDec 08 2016${\rm CTT}_{\rm qe}$ is a version of Church's type theory that includes quotation and evaluation operators that are similar to quote and eval in the Lisp programming language. With quotation and evaluation it is possible to reason in ${\rm CTT}_{\rm qe}$ ... More
Fixpoint Approximation of Strategic Abilities under Imperfect InformationDec 08 2016Model checking of strategic ability under imperfect information is known to be hard. In this paper, we propose translations of ATLir formulae that provide lower and upper bounds for their truth values, and are cheaper to verify than the original specifications. ... More
Clustered Cell Decomposition in P-Minimal StructuresDec 08 2016We prove that in a $P$-minimal structure, every definable set can be partitioned as a finite union of classical cells and regular clustered cells. This is a generalization of previously known cell decomposition results by Denef and Mourgues, which were ... More
Constructibility and Rosserizability of the Proofs of Boolos and Chaitin for Godel's Incompleteness TheoremDec 08 2016The proofs of Chaitin and Boolos for Godel's Incompleteness Theorem are studied from the perspectives of constructibility and Rosserizability. By Rosserization of a proof we mean that the independence of the true but unprovable sentence can be shown by ... More
Normalisation by Evaluation for Type Theory, in Type TheoryDec 07 2016We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or ... More
Efficient Certified RAT VerificationDec 07 2016Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called ... More
Efficient Certified RAT VerificationDec 07 2016Dec 08 2016Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called ... More
Quotient inductive-inductive typesDec 07 2016In type theory one usually defines data types inductively. Over the years, many principles have been invented, such as inductive families, and inductive-recursive and inductive-inductive definitions. More recently, higher inductive types have been proposed ... More
Imaginaries in separably closed valued fieldsDec 07 2016We show that separably closed valued fields of finite imperfection degree (either with lambda-functions or commuting Hasse derivations) eliminate imaginaries in the geometric language. We then use this classification of interpretable sets to study stably ... More
On Free ω-Continuous and Regular Ordered AlgebrasDec 07 2016Let E be a set of inequalities between finite {\Sigma}-terms. Let V_{\omega} and V_r denote the varieties of all {\omega}-continuous ordered {\Sigma}-algebras and regular ordered {\Sigma}-algebras satisfying E, respectively. We prove that the free V_r-algebra ... More
Topological Subset Space Models for BeliefDec 06 2016In recent work, Robert Stalnaker proposes a logical framework in which belief is realized as a weakened form of knowledge. Building on Stalnaker's core insights, we employ \emph{topological} tools to refine and, we argue, improve on this analysis. The ... More
Focusing in OrthologicDec 06 2016We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a very simple system relying on the involutive status of negation. The second one incorporates the ... More
"Boring formal methods" or "Sherlock Holmes deduction methods"?Dec 06 2016This paper provides an overview of common challenges in teaching of logic and formal methods to Computer Science and IT students. We discuss our experiences from the course IN3050: Applied Logic in Engineering, introduced as a "logic for everybody" elective ... More
Parametric equations for temporal style assertionsDec 06 2016Temporal logic provided an appealing approach to specifying properties of operating systems and other "reactive" software by making referencing the state graph implicitly. This paper shows how to get the same effect, with a finer control over specification ... More
Finite versus infinite: an insufficient shiftDec 05 2016The shift graph is defined on the space of infinite subsets of natural numbers by letting two sets be adjacent if one can be obtained from the other by removing its least element. We show that this graph is not a minimum among the graphs of the form $G_{f}$ ... More