We benchmark four proof assistants (Agda, Idris 2, Lean 4 and Rocq) through a single test suite. We focus our benchmarks on the basic features that all systems based on a similar foundations (dependent type theory) have in common. We do this by creating an "over language" in which to express all the information we need to be able to output correct and idiomatic syntax for each of our targets. Our benchmarks further focus on "basic engineering" of these systems: how do they handle long identifiers, long lines, large records, large data declarations, and so on. Our benchmarks reveals both flaws and successes in all systems. We give a thorough analysis of the results. We also detail the design of our extensible system. It is designed so that additional tests and additional system versions can easily be added. A side effect of this work is a better understanding of the common abstract syntactic structures of all four systems.

Discussions of game-related experiences are facilitated (and hampered) by the shared vocabulary and conceptual frameworks we have. Currently many such frameworks are heavily focused on players and mechanics, even though many other types of experience exist. The Experiential Tetrad (ExperT) is our conceptual framework encompassing a broader set of game-related experiences. ExperT is based on a synthesis of work on user, player and spectator experiences. We have used ExperT in our own work to help organize and classify existing literature, and it has also helped us find new avenues of research. While ExperT is not yet all-encompassing, we have already found it useful to clarify our discussions of experiential theories for games.

Rig groupoids provide a semantic model of Π , a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal and equationally sound and complete for a variety of gate sets. The first map corresponds to an 8th root of the identity morphism on the unit 1. The second map corresponds to a square root of the symmetry on 1 + 1 . As square roots are generally not unique and can sometimes even be trivial, the maps are constrained to satisfy a nondegeneracy axiom, which we relate to the Euler decomposition of the Hadamard gate. The semantic construction is turned into an extension of Π , called Π , that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to ≤ 2 qubits, and the computationally universal Gaussian Clifford+T gate set.

We construct a computationally universal quantum programming language Quantum Π from two copies of Π , the internal language of rig groupoids. The first step constructs a pure (measurement-free) term language by interpreting each copy of Π in a generalisation of the category Unitary in which every morphism is “rotated” by a particular angle, and the two copies are amalgamated using a free categorical construction expressed as a computational effect. The amalgamated language only exhibits quantum behaviour for specific values of the rotation angles, a property which is enforced by imposing a small number of equations on the resulting category. The second step in the construction introduces measurements by layering an additional computational effect.

Studying and developing systems that can recognize, express, and “have” emotions is calledaffective computing. To create a Computational Model of Emotion (CME), one must first identify what kind of system to build, then find emotion theories that match its requirements. The relevant literature is vast. This survey aims to help design CMEs thatgenerate emotions—separated intoemotion representationandelicitationtasks—in computer agents and interfaces. We give an overview of 67 CMEs from different domains, and identify which emotion theories they use and why. To better understand why CMEs use some theories, we also analyze instances where these CMEs use theories toexpress emotion. Lastly we summarize how CMEs generally use each theory. The survey is meant to be a guideline for deciding which affective theories to use for new emotion-generating CME designs.

The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.

How does one build a healthy gaming ecosystem? Recent evidence clearly demonstrates the existence of problematic gaming [1]. Predicting problematic gaming is still in its infancy. Here we focus on excessive gaming and model in-game behaviour as a means to continuously predict future play time. This can be used to help players maintain a healthy balance between the virtual and real worlds. To do this, we convert game log data into time-series and label such data with criteria of problematic gaming. Deep learning is then used to solve the resulting multi-class classification problem.

Programming languages with sufficiently expressive type systems provide users with different means of data ‘bundling’. Specifically, in dependently-typed languages such as Agda, Coq, Lean and Idris, one can choose to encode information in a record either as a parameter or a field. For example, we can speak of graphs over a particular vertex set, or speak of arbitrary graphs where the vertex set is a component. These create isomorphic types, but differ with respect to intended use. Traditionally, a library designer would make this choice (between parameters and fields); if a user wants a different variant, they are forced to build conversion utilities, as well as duplicate functionality. For a graph data type, if a library only provides a Haskell-like typeclass view of graphs over a vertex set, yet a user wishes to work with the category of graphs, they must now package a vertex set as a component in a record along with a graph over that set.

Probabilistic programming languages are valuable because they allow domain experts to express probabilistic models and inference algorithms without worrying about irrelevant details. However, for decades there remained an important and popular class of probabilistic inference algorithms whose efficient implementation required manual low-level coding that is tedious and error-prone. They are algorithms whose idiomatic expression requires random array variables that are latent or whose likelihood is conjugate . Although that is how practitioners communicate and compose these algorithms on paper, executing such expressions requires eliminating the latent variables and recognizing the conjugacy by symbolic mathematics. Moreover, matching the performance of handwritten code requires speeding up loops by more than a constant factor. We show how probabilistic programs that directly and concisely express these desired inference algorithms can be compiled while maintaining efficiency. We introduce new transformations that turn high-level probabilistic programs with arrays into pure loop code. We then make great use of domain-specific invariants and norms to optimize the code, and to specialize and JIT-compile the code per execution. The resulting performance is competitive with manual implementations.

Direct reflection is a form of meta-programming in which program terms can intensionally analyze other program terms. Previous work defined a big-step semantics for a directly reflective language called Archon, with a conservative approach to variable scoping based on operations for opening a lambda-abstraction and swapping the order of nested lambda-abstractions. In this short paper, we give a small-step semantics for a revised version of Archon, based on operations for opening and closing lambda abstractions. We then discuss challenges for designing a static type system for this language, which is our ultimate goal.

We present the design and implementation of a generative geometric kernel. The kernel generator is generic, type-safe, parametrized by many design-level choices and extensible. The resulting code has minimal traces of the design abstractions. We achieve genericity through a layered design deriving concepts from affine geometry, linear algebra and abstract algebra. We achieve parametrization and type-safety by using OCaml's module system, including higher order modules. The cost of abstraction is removed by using MetaOCaml's support for code generation coupled with some annotations atop the code type.

The steady rise in interest in formal verification of software has naturally been accompanied by increased interest in the theory and tools of verification.While there are many textbooks of logic as well as user guides for the vast array of reasoning tools (automated and otherwise), much less is written about how to bridge the two, never mind good guides to the design problems of building reasoning tools.Harrison's Handbook of Practical Logic and Automated Reasoning explores that gap with flair.Even a casual glance at this hefty 700 page book will quickly dispel any "Handbook" impression which the title disingenuously gives: not a handbook at all, but rather a proper textbook.The style, far from that of a reference book, is deeply pedagogical, complete with a significant set of well-crafted exercises.It is well written using lucid prose, with the author taking great pains to elucidate important points, pausing to illustrate some subtleties, as well as being rather erudite in its coverage of the relevant literature, both historical and contemporary.As a textbook style introduction to the theory and practice of (first order, mathematical) logic and automated reasoning, it succeeds beautifully.This textbook masterfully weaves together theory and practice, by interleaving the development of the theoretical underpinnings of each topic covered with fairly well crafted code which implements the constructive portions of each chosen topic.In other words, this textbook is also a literate program, with all code written in OCaml, available from Harrison's web site.This really forces the author to cover many topics which are often, regrettably, omitted from other "practical" introductions to logic.Readers primarily interested in the theory covered by this book may find this aspect distracting, but I rather view this aspect of the book as one of its more endearing characteristics.The prose aspects of this literate textbook could easily serve as a model for years to come.The code is written using a fairly small subset of the Objective Caml language (no objects, Functors, higher rank polymorphism, nor polymorphic variants).While higher-order functions abound, the author nevertheless does not make heavy use of a more combinator-driven style which is more prevalent in the current functional literature.Eschewing Functors also means that the higher abstractions frequently seen in modern functional programs are also not used.While such a choice does broaden the audience which can easily understand the code, it would nevertheless be quite interesting to redevelop the same code, first in idiomatic Haskell, and then in Agda.But doing this would surely result in a research-level monograph, which was clearly not the author's intent.In other words, while this text does not use the most modern functional programming idioms, this was clearly an explicit decision, which makes sense in the context of the audience for this book.The set of topics covered might seem somewhat eclectic: propositional logic, first-order logic, equality reasoning, decidable problems, interactive theorem-proving and the limitations of all these approaches.In particular, "decidable problems" and "interactive theorem-proving" have traditionally been seen as belonging in different universes by the more "pure" adherents of formal reasoning.Of course, there have always been systems which eschewed this particular balkanisition, with ACL2, IMPS and PVS immediately coming to mind, and Harrison's own HOL Light following in the tradition.But this is now changing, as traditionally very pure

Abstract We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.

We define a canonical form for piecewise defined functions. We show that the domains and ranges for which these functions are defined is larger than in previous work. Also, our canonical form algorithm is linear in the number of breakpoints instead of exponential. These results rely on the linear structure of the underlying domain of definition.

Having been convinced of the potential benefits of partial evaluation, we wanted to conduct some experiments in our favourite Computer Algebra System, Maple. Maple is a large language, with a few non-standard features. When we tried to implement a partial evaluator for it, we ran into a number of difficulties for which we could find no solution in the literature. Undaunted, we persevered and ultimately implemented a working partial evaluator with which we were able to very successfully [11] conduct our experiments. In this paper, we document the techniques we had to either invent or adapt to achieve these results.

We give the first formal definition of the concept of simplification for general expressions in the context of Computer Algebra Systems. The main mathematical tool is an adaptation of the theory of Minimum Description Length, which is closely related to various theories of complexity, such as Kolmogorov Complexity and Algorithmic Information Theory. In particular, we show how this theory can justify the use of various "magic constants" for deciding between some equivalent representations of an expression, as found in implementations of simplification routines.