Logic and Semantics Seminar

In information-theoretic terms, a map is continuous when a finite amount of information about the input suffices for computing a finite amount of information about the output. Already Brouwer observed that this allows one to represent a continuous functional from sequences to numbers with a certain well-founded question-...

Observational Type Theory is an internal language for types equipped with a proof-irrelevant propositional equality. As such, it natively supports extensionality principles, UIP, and quotients of types by proof irrelevant relations (à la Lean). Unfortunately, it is difficult to use these quotients without any choice...

In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many (most) synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples...

We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the...

Memory consistency specifications (MCSs) are a difficult, yet critical, part of a concurrent programming framework. Existing MCS testing tools are not immediately accessible, and thus, have only been applied to a limited number of devices. However, in the post-Dennard scaling landscape, there has been an explosion of new...

In recent work on discrete neural networks, I considered such networks whose activation functions are polymorphisms of finite, discrete relational structures. The general framework I provided was not entirely categorical in nature but did provide a steppingstone to a categorical treatment of neural nets which are...

This paper presents recent work on the Luau programming language which is used for, amongst other reasons, scripting games. We talk about the human aspects of the Luau type system, and in particular, how large the heterogeneous developer community is for Luau. We then talk about two recent developments in Luau, in...

Choreographic programming is an emerging paradigm for message-passing concurrency. A choreographic program (or "choreography") describes the computation of an entire system; this ensures deadlock-freedom without requiring the extraneous checks that other solutions like session types require. Choreographies seem perfect for...

We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of...

Mathematical models of disease are important and widely used, but building and working with these models at scale is challenging. Many epidemiologists use “stock and flow diagrams” to describe ordinary differential equation (ODE) models of disease dynamics. This talk introduces the mathematics of stock and flow diagrams...