ABSTRACT. Gradually typed languages, including Typed Racket, Typescript, Thorn and Reticulated Python, facilitate interoperability between statically and dynamically typed code, by checking static types when available and applying dynamic type checks when not. However, almost all exisiting research studies gradually typed languages using operational semantics, designed in an ad hoc manner. Furthermore, in the operational setting, questions of program equivalence and other relational properties are difficult to study and for the most part ignored.

In this paper, we propose a type-theoretic and category-theoretic semantics for gradual typing, in the form of gradual type theory, a logic and type theory for (call-by-name) gradual typing. To define the central constructions of gradual typing (the dynamic type, type casts and type error) in a type-theoretic fashion, we extend the theory of types and terms to include gradual type and term precision, internalizing notions of ``more dynamic'' into the type theory and then using these to characterize the constructions of gradual typing uniquely. This includes a novel specification for casts in terms of type and term precision. Combined with the ordinary extensionality ($\eta$) principles that type theory provides, we show that most of the standard operational behavior of casts in a gradually typed language are in fact uniquely determined by our design constraints. This provides a semantic justification for the definitions of casts and also shows that non-standard definitions of casts must violate these principles. We explore a call-by-name type theory in this paper, because it is a simple setting with the necessary extensionality principles, leaving call-by-value to future work.

On the category-theoretic side, we show that our type theory is an internal language of a certain class of double categories called called equipments (in fact, we will use only preorder categories, which are double categories where one direction is posetal), which provides the right algebraic structure with which to interpret precision and casts in gradual typing. We apply this categorical semantics to give a general construction of models of gradual typing, which provides a semantic analogue of Findler and Felleisen's definitions of contracts, and generalizes Dana Scott's domain-theoretic models of dynamic typing.

ABSTRACT. Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, encoding productivity in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of type checking. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types.

The main challenge for constructing this model is to model the notion of ticks used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion, but in this category there is no object of ticks, so tick-assumptions in a context can not be modelled using standard tools. Instead we show how ticks can be modelled using adjoint functors, and how to model the tick constant using a semantic substitution.

ABSTRACT. We 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 by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to a completely internal development of models of homotopy type theory within what we call crisp type theory.

ABSTRACT. In this paper we define a framework to address different kinds of problems related to type inhabitation, such as type checking, the emptiness problem, generation of inhabitants and counting, in a uniform way. Our framework uses an alternative representation for types, called the pre-grammar of the type, on which different methods for these problems are based. Furthermore, we define a scheme for a decision algorithm that, for particular instantiations of the parameters, can be used to show different inhabitation related problems to be in PSPACE.

ABSTRACT. In order to avoid well-know paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type{0} : Type{1} : .... Such type systems are called cumulative if for any type A we have that A : Type{i} implies A : Type{i+1}. The Predicative Calculus of Inductive Constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system.

In this paper we present the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) which extends the cumulativity relation to inductive types. We discuss cumulative inductive types as present in Coq 8.7 and their application to definitional translations.

ABSTRACT. We present Tores, a language for logical reasoning which utilizes indexed types and flexible (co)recursion principles to allow encoding of metatheoretic proofs. We particularly target the encoding of proofs using the technique of logical relations. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types together with a form of recursion over objects in the index language to build new types. The latter, which we call index-stratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination.

ABSTRACT. While the theory of functional higher-order languages, starting from lambda-calculi, is a well-established research field, it is only in recent years that the operational semantics of higher-order languages with probabilistic operators has started to be extensively studied. A fundamental notion in the semantics of programming languages is that of program equivalence. In higher-order languages, program equivalence is generally formalized as a contextual equivalence, which can be hard to prove directly. This has motivated the study of proof techniques for contextual equivalence, from inductive ones, such as logical relations, to coinductive ones, mainly in the form of bisimulations. In this talk I will discuss proof techniques for program equivalence in languages combining higher-order and probabilistic features. Several operational methods, traditionally developed in a deterministic setting, have been adapted to probabilistic higher-order languages. I will discuss these proof methods and focus on bisimulation-based techniques, showing how probabilities, combined with different language features, force a number of modifications to the definition of bisimulation.

ABSTRACT. Higher inductive-inductive types (HIITs) generalise inductive types of dependent type theories in two directions. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalising higher inductive types of homotopy type theory. An example which makes use of both features is the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a domain-specific type theory. A context in this small type theory encodes a HIIT by listing the type formation rules and constructors. The type of the elimination principle and its beta-rules are computed from the context using a variant of the syntactic logical relation translation. We show that for indexed W-types and various examples of HIITs the computed elimination principles are the expected ones. Showing that the thus specified HIITs exist is left as future work. The type theory specifying HIITs was formalised in Agda together with the syntactic translations. A Haskell implementation converts the types of sorts and constructors into valid Agda code which postulates the elimination principles and computation rules.

ABSTRACT. Environments and closures are two of the main ingredients of evaluation in lambda-calculus. A closure is a pair consisting of a lambda-term and an environment, whereas an environment is a list of lambda-terms assigned to free variables. In this paper we investigate some dynamic aspects of evaluation in lambda-calculus considering the quantitative, combinatorial properties of environments and closures. Focusing on two classes of environemnts and closures, namely the so-called plain and closed ones, we consider the problem of their asymptotic counting and effective random generation. We provide an asymptotic approximation of the number of both plain environments and closures of size n. Using the associated generating functions, we construct effective samplers for both classes of combinatorial structures. Finally, we discuss the related problem of asymptotic counting and random generation of closed environemnts and closures.

ABSTRACT. We show that LOGSPACE is characterised by finite orthogonal tail-recursive cons-free constructor term rewriting systems. This result is non-trivial, because in contrast to previous work on characterising LOGSPACE by tail-recursive cons-free programs we do not impose any fixed evaluation strategy. We provide a LOGSPACE algorithm which computes constructor normal forms. We then use this algorithm in the proof of our main result: that simple stream term rewriting systems characterise LOGSPACE-computable stream functions as defined by Ramyaa and Leivant. This result concerns characterising logarithmic-space computation on infinite streams by means of infinitary rewriting.

ABSTRACT. Logic and probability are ancient subjects whose unification holds significant potential for the field of artificial intelligence. The BLOG (Bayesian LOGic) language provides a way to write probability models using syntactic and semantic devices from first-order logic. In modern parlance, it is a relational, open-universe probabilistic programming language that allows one to define probability distributions over the entire space of first-order model structures that can be constructed given the constant, function, and predicate symbols of the program. In this public lecture, Stuart Russell will describe the language mainly through examples and cover its application to monitoring the Comprehensive Nuclear-Test-Ban Treaty.