38 citations · 103 across the 14 of their papers we have counts for
15 papers
Generalized Decidability via Brouwer Trees
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh +1
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable…
Constructive Ordinal Exponentiation
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
In classical mathematics, ordinal arithmetic is well-studied; constructively, addition and multiplication are well-known. We study constructive ordinal exponentiation, where ordina…
Responsible Composition and Optimization of Integration Processes under Correctness Preserving Guarantees
Daniel Ritter, Fredrik Nordvall Forsberg, Stefanie Rinderle-Ma
Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scena…
Set-Theoretic and Type-Theoretic Ordinals Coincide
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary…
Type-Theoretic Approaches to Ordinals
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate li…
Translating Extensive Form Games to Open Games with Agency
Matteo Capucci, Neil Ghani, Jérémy Ledent +1
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion…
Connecting Constructive Notions of Ordinals in Homotopy Type Theory
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and…
Compositional Game Theory, Compositionally
Robert Atkey, Bruno Gavranović, Neil Ghani +3
We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules,…
Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law
Neil Ghani, Clemens Kupke, Alasdair Lambert +1
We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show th…
Three Equivalent Ordinal Notation Systems in Cubical Agda
Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani
We present three ordinal notation systems representing ordinals below in type theory, using recent type-theoretical innovations such as mutual inductive-inductive d…
Catalog of Optimization Strategies and Realizations for Composed Integration Patterns
Daniel Ritter, Fredrik Nordvall Forsberg, Stefanie Rinderle-Ma +1
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integra…
A Compositional Treatment of Iterated Open Games
Neil Ghani, Clemens Kupke, Alasdair Lambert +1
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be…
Quotient inductive-inductive types
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra +2
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotien…
Positive Inductive-Recursive Definitions
Neil Ghani, Fredrik Nordvall Forsberg, Lorenzo Malatesta
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive induc…
Extracting verified decision procedures: DPLL and Resolution
Ulrich Berger, Andrew Lawrence, Fredrik Nordvall Forsberg +1
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability…