Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form ####Sn = ####Sn. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has Z/2Z as fundamental group. For the latter result, we develop an EHP long exact sequence.

We solve in polynomial time two decision problems that occur in type checking when typings depend on universe level constraints.

Abstract We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.

We give a constructive proof of Skolem’s Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.

In this note we show that Voevodsky’s univalence axiom holds in the model of type theory based on cubical sets as described in Bezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, vol 26, pp 107–128, 2014. https://doi.org/10.4230/LIPIcs.TYPES.2013.107 . http://drops.dagstuhl.de/opus/volltexte/2014/4628 ) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan’s construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.

The Skolem machine is a Turing-complete machine model where the instructions are first-order formulas of a specific form. We introduce Skolem machines and prove their logical correctness and completeness. Skolem machines compute queries for the Geolog language, a rich fragment of first-order logic. The concepts of Geolog trees and complete Geolog trees are defined, and these tree concepts are used to show logical correctness and completeness of Skolem machine computations. The universality of Skolem machine computations is demonstrated. Lastly, the paper outlines implementation design issues using an abstract machine model approach.

Abstract We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Gödel's Dialectica interpretation.

Abstract This paper reports on the first steps towards the formal verification of correctness proofs of real-life protocols in process algebra. We show that such proofs can be verified, and partly constructed, by a general purpose proof checker. The process algebra we use isμCRL, ACPτaugmented with data, which is expressive enough for the specification of real-life protocols. The proof checker we use is Coq, which is based on the Calculus of Constructions, an extension of simply typed lambda calculus. The focus is on the translation of the proof theory ofμCRL andμCRL-specifications to Coq. As a case study, we verified the Alternating Bit Protocol.

Capsule ReviewIt had been known that the simplest system with dependent types, XP, is undecidable, in that sense that the set {(A,D\3pr\-XP p:A} is non-computable.The proof runs as follows.First, there is an obvious embedding of predicate logic into XP.This is the principle idea of one of the basic members of the AUTOMATH family, AUT-QE, and also later of Edinburgh LF.It can be shown that this embedding is conservative (Berardi; Barendsen and Geuvers).This is not completely obvious, since XP has functions of arbitrarily high type at its disposal.Now it follows from Godel's technique (proving the incompleteness theorems) that arithmetic and even a finitely axiomatizable part of it (Robinson's arithmetic) is essentially undecidable.Therefore XP is also undecidable.This is quite a long path to the result -admittedly quite beautiful, passing along classical details like the Chinese remainder theorem -but almost too much.Fortunately, the authors of this paper have given a very direct argument showing the same result, by a surprisingly straightforward encoding of a register machine.An inhabitation problem in a given Pure Type System (PTS) XS is a pair (F, B) such that, for some sort s, F \-^s B : s.A solution for (F, B) is a term A such that F \~xs A : B. In this note we prove that in the PTS kP it is undecidable whether an inhabitation problem has a solution.This result also follows from Lob's results on embeddings of predicate logic in fragments of intuitionistic logic (Lob, 1976, p. 1, 1. 10) plus the fact that XP is sound and complete with respect to minimal predicate logic (see Geuvers (1993)).The merit of our proof is that it is short, simple and intuitive.Sometimes, inhabitation problems are defined with F the empty context.In IP, however, this makes little sense: the only statement valid in the empty context is * : D. After the proof of our result, we discuss related results concerning the other systems of the ^-cube.For a general introduction to PTSs the reader is referred to Barendregt (1992).

We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in μCRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complicated. The complexity has been mastered by explicitly identifying invariants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.

Consistency of a knowledge-based system has become a topic of growing concern. Of course, consistency is closely related to a notion of semantics. We present a theoretical framework in which both the semantics and the consistency of a knowledge base can be studied. This framework is based on first-order flat many-sorted predicate logic and is sufficiently rich to capture an interesting class of rule-based expert systems and deductive databases. We analyse the feasibility of the consistency test and prove that this test is feasible for knowledge bases in Horn format without quantification.

The main result of this paper will be that various notions of majorizability and compactness coincide in the full typestructure over the natural numbers. Moreover we shall show that the extensional typestructure of strongly majorizable functionals can be obtained by applying Zucker's construction ( )E to any of these coinciding intensional typestructures. A different result is proved in the typestructure of effective operations, where not every majorizable functional is compact. Finally we shall introduce the concept of relative compactness in the full typestructure and prove that there are just two degrees of compactness.

Abstract In this paper it will be shown that HEO and HROE are isomorphic with respect to extensional equality. This answers a question of Troelstra [T, 2.4.12, p. 128]. The main problem is to extend effective operations to a larger domain. This will be achieved by a modification of the proof of the continuity of effective operations. Following a suggestion of A. S. Troelstra, similar results were obtained for ECF(U) and ICFE(U), where U is any universe of functions closed under “recursive in”.

Abstract In this paper a model for barrecursion is presented. It has as a novelty that it contains discontinuous functionals. The model is based on a concept called strong majorizability. This concept is a modification of Howard's majorizability notion; see [T, p. 456].