A Constructive Cellular Approximation Theorem in HoTT
ABSTRACT. In this work, we revisit the definition of CW complexes that was given by Favonia and Buchholtz, and we develop their theory. In particular, we focus on the cellular approximation theorem, a cornerstone result in Algebraic Topology which says that maps between CW complexes and their homotopies may be approximated by maps and homotopies that respect the cellular structure. We give a constructive proof of the theorem that relies heavily on the (admissible) principle of finite choice, and we discuss the extent to which the theorem can be strengthened while remaining constructive.
Representing Temporal Operators with Dependent Event Types
ABSTRACT. Event semantics were first proposed and studied by Davidson to express the occurrence of events in order to find suitable semantics for describing both actions and adverbial modifications, and further studied and developed by many in the fields of logic, philosophy and computer science. Later works showed that dependent types theories were suitable for formalising event semantics in the form of dependent event types, which allow for selection restriction through semantic roles such as the agent of an event.
In this work, we propose a further refinement of dependent event types by extending a type system with dependent event types by arbitrary semantic roles. We show that in the case of Church’s simple type theory with dependent event types, this extension by arbitrary semantic roles is conservative. We focus on the semantic role of time via the introduction of a timeline type Time and subtypes of events parameterised by a timestamp, and use this to formulate traditional temporal operators and explore their properties in this system.
Normalization of Natural Deduction for Classical Predicate Logic
ABSTRACT. Normalization for natural deduction has been studied a lot, starting from the work of Gentzen and especially Prawitz. The idea is that a deduction can be transformed into one in "normal form" which has the sub-formula property: every formula used in a normal deduction is a sub-formula of the conclusion or of one of the hypotheses. The sub-formula property also implies that the rules for the connectives are self-contained: a deduction of a formula involving (for example) only -> does not require other connectives. For constructive logic, the idea of normalization is to eliminate detours: an introduction rule followed by an elimination rule. For classical predicate logic, the situation is more subtle and e.g. Prawitz [1965] restricts the logic and Statman [1974] restricts the ways in which the rules can be applied.
We give a proof of normalization of natural deduction for classical predicate logic using our earlier work on truth-table natural deduction (TT-ND, Geuvers Hurkens [2022]). TT-ND gives a general format for propositional deduction rules and uses a term-interpretation of deductions to study normalization. We instantiate the general TT-ND format for the case of the well-known connectives (/\, \/, ->, ~) and we add the quantifiers forall and exists. For the quantifiers we use classical rules, using "witnesses". We show normalization by exhibiting a proof-term-reduction procedure that terminates and we show that normal deductions have the sub-formula property.
Similar approaches to natural deduction, using so called "generalized" introduction and elimination rules, can be found, a.o., in the work of von Plato and Sieders [2012], Milne [2015], Kurbis [2021, 2022] and Shangin [2023]. Our approach is specific as it uses classical rules for the quantifiers and can be flexibly adapted to include (or exclude) specific connectives. It also gives the unrestricted sub-formula property for normal deductions.
ABSTRACT. The focus of our work lies in enhancing the semantic understanding of useful open CBV, from a quantitative point of view. For this, we propose a quantitative interpretation for an inductive formulation of useful open CBV, based on non-idempotent intersection types. We equip this type system with a notion of tightness, and we show that the inductive definition of useful evaluation is sound and complete, meaning in particular that for any tight type derivation of a program t with independent counters m and e, the term t evaluates to a normal form in exactly m function application steps and e substitution steps. This is a novel result in the literature, as existing useful evaluation notions lack semantic interpretations, and existing quantitative interpretations do not consider usefulness.
Splitting Booleans with Normalization-by-Evaluation
ABSTRACT. Is the equational theory induced by extensional sum types A + B decidable ?
This problem has a positive answer with simple types but is open in presence of
type dependency. We investigate a simple type theory PiBoolExt featuring
extensional booleans and report on a toy OCaml implementation of a typechecker
based on normalization-by-evaluation (NbE).
Implementing Observational Equality with Normalisation by Evaluation
ABSTRACT. We report on an experimental implementation of a type theory with an observational equality type, based on Pujet and Tabareau's CCobs, extended with a form of inductive and quotient types. It features a normalisation by evaluation function, which is used to implement a bidirectional type checker. We also explore proof assistant features, notably the interaction of strict propositions with meta-variables, and a rudimentary “hole” system.
Towards a logical framework modulo rewriting and equational theories
ABSTRACT. Dedukti is a logical framework based on a dependent type theory extended with user-defined rewrite rules. It can be used to encode a wide variety of systems, yet some features of proof systems remain out of reach. Among them we find universes that seem hard to encode with a confluent rewriting system, typically due to non-linear and non-terminating rules such as those pertaining to the maximum of universe levels. In practice this causes problems when encoding the type theories of Agda, Coq or Lean. Another important theory that is hard to encode using only rewrite rules is the relatively recent cubical type theory in which type-checking requires deciding the inclusion of hypercube faces expressed in an algebraic structure related to de Morgan algebra.
To better support such theories, we argue for an extension of Dedukti in which one can augment the definitional equality not only with rewrite rules, but also with equational theories, which are sets of non-oriented equations. In this talk we will identify potential steps to take towards that goal as well as pitfalls that should be avoided. This work is still in a very early stage and the goal would be to eventually reach a logical framework with user-provided decidable theories.
Comodule Representations of Second-Order Functionals
ABSTRACT. In this work we demonstrate that the well-known approach of representing continuous second order functionals in terms of well-founded question-answer trees is an instance of a general compositional category-theoretic framework in which representations of second-order functionals are modulated by a monad on containers and a certain right comodule for it. By varying the monad and the comodule we naturally capture in the same framework standard tree-represented functionals, as well as many others, such as: functionals with finite support; functionals that query their input on one instance; functionals that either query the input once or indicate that no query is needed; and instance reductions as studied in reverse constructive mathematics and Weihrauch reducibility.
ABSTRACT. Already in the paper introducing the effective topos, Hyland pointed out an interesting connection between computability theory and realizability: the Turing degrees embed into the lattice of subtoposes of the effective topos. I'll talk about a modern approach to this same idea, where we replace topos theory with homotopy type theory, and the effective topos with cubical assemblies.