ABSTRACT. Homotopy Type Theory is an extension of MLTT that allows us to study ideas from topology by re-expressing them a synthetic language. For example, paths are modeled by terms of equality types. The synthetic nature allows one to manipulate the nuts and bolts of homotopy theory directly, keeping a strong connection to the geometric ideas.

With the desire to gain better insight into how to approach homotopy theory in HoTT, we set out to prove that there is no degree one map from a closed oriented genus g surface to a closed oriented genus h surface if g < h. Although we have not reached that destination, along the way we have proved synthetic versions of some classical results.

Building on Hou (Favonia) and Harper's results on covering spaces, we prove HoTT versions of the lifting criterion and the classification of covering spaces. Secondly, we investigated for which connected types X there exist canonical change-of-basepoint isomorphisms between its fundamental groups a different base points. Large parts of the theory are formalized in Coq.

ABSTRACT. Extended abstract

ABSTRACT. Dynamic type theory is a model of type theory which is based on the potentialist’s point of view. It has stages for each type and a refinement of type declarations, called state declarations, defining input and output bounds.

ABSTRACT. Martin-Löf type theory MLTT was extended by Setzer with a large universe type called a Mahlo universe, in order to provide MLTT with an analogue of some large cardinal property. Another instance of constructive systems extended with an analogue of some large set was formulated for Aczel's constructive set theory CZF: Rathjen, Griffor and Palmgren introduced an extension of CZF with the existence of inaccessible sets of all transfinite orders. It is not known whether this extension of CZF is interpretable in Setzer's MLTT with one Mahlo universe. Specifically, it is an open question how to interpret the transfinite hierarchy of inaccessible sets by using the reflection property of a Mahlo universe. As a step towards the interpretation, we show that the hierarchy of the types of iterative sets, which Rathjen, Griffor and Palmgren defined as the type-theoretic counterpart for inaccessible sets of transfinite orders, can be defined by means of the Mahlo universe.

ABSTRACT. Working in homotopy type theory, we present and compare several possible definitions of the property that a given (untruncated) semicategory has identities.

ABSTRACT. We report on some new observations regarding the constructive reverse mathematics of first-order completeness theorems. When conducted in a constructive type theory such as the calculus of inductive constructions (CIC), many different formulations of completeness can be distinguished and analysed regarding their sufficient and necessary non-constructive assumptions. As the main new result, we identify a principle we dub WLEMS at the intersection of double-negation shift and weak excluded middle, exactly capturing the non-constructivity needed for object-level disjunctions. The observations reported here are part of an ongoing general attempt at a systematic classification of the independent ingredients contributing to the non-constructivity of completeness theorems.

ABSTRACT. Differential dynamic logic is a formal framework to specify and reason about hybrid programs (HPs). The core of dL is a proof calculus that contains a collection of axioms and rules for the rigorous verification of properties of HPs. Recently, dL has been embedded within the theorem prover Prototype Verification System (PVS) resulting in the tool Plaidypvs2. The integration of dL into PVS expands its expressive power; user defined functions, such as trigonometric and other transcendental functions, can be used inside the dL framework, and meta-reasoning about HPs can be performed, including reasoning about entire classes of HPs, specified using dependent types in PVS. The differential temporal dynamic logic (dTL2) extends dL with temporal logic operators to reason about all the states reachable during the execution of an HP. This paper presents a work in progress focusing on embedding dTL2 in PVS as an extension of Plaidypvs. Plaidypvs is expanded with the formalization of a trace semantics for HPs, the definition of the LTL temporal operators eventually and globally, and the implementation of the proof calculus for dTL2. This new embedding has the same capabilties as Plaidypvs, which allows user defined functions and meta-reasoning of properties of HPs. To the best of the authors’ knowledge this is the first implementation of dTL2.

ABSTRACT. In proof assistants based on dependently-typed languages, record types have been used as interfaces for abstraction bundling some objects, including mathematical structures. However, these record types introduce some indirections, namely, constructions and destructions of records, which can be a source of efficiency and intelligibility issues in translations such as extraction and parametricity translation. We propose a translation from Coq to Coq that expands record types and eliminates these indirections.

ABSTRACT. Category Theory is a very active domain in both computer science and math- ematics research, with applications from algebraic geometry to programming languages design. Many attempts to formalize parts of this field in proof assistants have been made. However, categorical reasoning often involves a graphical abstraction, called diagrams, that are complicated to emulate in text based proof assistant. We propose an interface as a Coq plugin that allows extracting such a diagram from the Coq proof state, allowing to alternate between graphical steps and usual tactic steps to produce categorical proofs.

ABSTRACT. The aim of this work is to combine profinite methods and models of the λ-calculus to obtain a notion of profinite lambda-term which, we show, lives in perfect harmony with the principles of Reynolds parametricity. This is joint work with Sam van Gool and Paul-André Melliès.

ABSTRACT. The idea of combinatory logic synthesis (CLS) is: Given a repository Gamma of combinators typed by intersection types and an intersection type tau, construct combinatory terms M such that M is assigned the type tau wrt. Gamma in Finite Combinatory Logic. A notable weakness of intersection types as synthesis query language is the inability to express negative information. We propose a Boolean extension to CLS, adding the connectives AND, OR, and NOT to the query language. This results in a stratified type system, consisting of finite combinatory logic and (partly) a monomorphic variant of a set-theoretic type system. We implement and compare two distinct inhabitation procedures for the presented stratified type system.

ABSTRACT. Python has become a popular language in the last few years, being adopted by entry-level programmers all the way to data scientists. Due to this widespread adoption, a trustworthy Python execution machinery should be critical and valuable. However, the language lacks a comprehensive formal definition that could provide provable guarantees and serve as basis for a verified implementation. One of the reasons is that formalizing a language of the size and complexity of Python requires a lot of effort and expertise. Moreover, as the language is evolving fast, an existing formalization would need to be reviewed and possibly modified at each new release.

We propose that, since Python's virtual machine executes bytecode and does not interpret Python's source code directly, an alternative direction towards a verified Python implementation is to start from this lower, and smaller and more stable, level. Therefore, we present a formalization of Python's bytecode and virtual machine execution. Our formalization uses inference rules to define typing of objects and semantics, which includes execution of bytecode and management of the frame stack. The proposed rules are shown to satisfy progress and preservation. In addition, our proposed framework can be extended with built-in types without breaking safety guarantees. The formalized rules were implemented in fstar, where properties about them can be proved automatically via dependent types or lemmas solved by an SMT solver. From the fstar implementation, we extracted an OCaml code that is able to execute Python bytecode. This verified Python execution machinery was compared to cpython for both consistency and performance.

ABSTRACT. Bisimulations and game techniques for higher-order languages have proved to be powerful tools for reasoning about program equivalence and building models that scale to advanced features such as side effects or existential types. Yet, their usage in mechanized proofs is rare. In this work in progress, we argue that this observation is, in part, the consequence of several mismatches between the traditional presentation of games in set theory and idiomatic constructions from type theory. We hence present a formulation of games and strategies more amenable to manipulation in proof assistants. The framework we propose is structured around a coinductive representation of labelled transition systems (LTS), inspired by the Coq library of interaction trees, and building upon the work of Levy and Staton. Our main contribution is to provide a unified account of operational game semantics (OGS), an LTS-based game model for which we prove the correctness of the generated bisimulation with respect to contextual equivalence. The construction, and the proof, are parametrized by a rather loose notion of evaluator assumed to satisfy a succinct axiomatization. In this talk, we will focus on (1) introducing the standard approach of operational game semantics succinctly, before (2) giving a more detailed account of the peculiarities and advantages of our representation of games and strategies.

ABSTRACT. We describe a formalization of a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation on the basis of any given multi-sorted binding signature. The construction is done in category theory (notably by using monoidal categories) whose formalization is in turn done in the Coq proof assistant, through the UniMath library of univalent mathematics.

ABSTRACT. Categorical Logic is a branch of mathematical logic which uses the concepts and tools of category theory to investigate logical systems and deductive calculi, following in the example of Lawvere’s pioneering work on functorial semantics for algebraic theories. In this talk, we’ll provide a progress report on a formalization of categorical logic in the Lean proof assistant.

ABSTRACT. Various kinds of structured categories are used to study the semantics of various flavors of type theory. For example, cartesian closed categories and symmetric monoidal closed categories are used to study the semantics of simple and linear type theory, respectively \cite{Benton94,mellies2009categorical}. Such categories represent models of the theory in study, whereas the initial such model represents the syntax.

If we would like to replicate this idea in univalent foundations, then we stumble on a difficulty, namely constructing the initial model. The reason for that comes from the fact that in univalent foundations, the correct notion of a category is a univalent category. If one uses the usual presentation of the syntax (of, for example, the simply typed lambda calculus), then the acquired cartesian closed category is not guaranteed to be univalent. As such, one needs to do some extra work to acquire the desired initial model.

The solution for our problem, lies in what is known as the \emph{Rezk completion}. In \cite{rezk_completion}, it is shown how every category is weakly equivalent to a univalent category. However, in that paper, preservation of categorical structure under Rezk completion is not considered. More concretely, if a category has a cartesian closed or a symmetric monoidal structure, can we say the same about its Rezk completion?

The goal of this abstract is to study the Rezk completion of categories with some additional structure. More specifically, our goal is to show how, for some notion of structure, the Rezk completion of a category preserves the structure.

ABSTRACT. We show how to strictify the intrinsic quotiented syntax of type theory such that the substitution laws (naturality laws) become definitional. The method was formalised in Agda for the case of simple type theory defined using simply types category with families. This is an example of a quotient inductive-inductive-recursive type.