64 citations · 157 across the 11 of their papers we have counts for
12 papers
Topos-Theoretic Approaches to Quantum Theory
Matthijs Vákár
This review paper surveys work by Isham, Butterfield, Döring, Landsman, Spitters, Heunen, and others on topos-theoretic analyses of quantum theory. It aims to provide a synthesized…
Principal Bundles and Gauge Theories
Matthijs Vákár
This set of lecture notes first gives an introduction to the geometry of principal bundles. Next, it demonstrates how they can be used to formalize the concept of gauge theories ar…
Conditional independence by typing
Maria I. Gorinova, Andrew D. Gordon, Charles Sutton +1
A central goal of probabilistic programming languages (PPLs) is to separate modelling from inference. However, this goal is hard to achieve in practice. Users are often forced to r…
Slamming the sham: A Bayesian model for adaptive adjustment with noisy control data
Andrew Gelman, Matthijs Vákár
It is not always clear how to adjust for control data in causal inference, balancing the goals of reducing bias and variance. We show how, in a setting with repeated experiments, B…
A Domain Theory for Statistical Probabilistic Programming
Matthijs Vákár, Ohad Kammar, Sam Staton
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languag…
Denotational validation of higher-order Bayesian inference
Adam Ścibior, Ohad Kammar, Matthijs Vákár +7
We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inferenc…
In Search of Effectful Dependent Types
Matthijs Vákár
Real world programming languages crucially depend on the availability of computational effects to achieve programming convenience and expressive power as well as program efficiency…
An Effectful Treatment of Dependent Types
Matthijs Vákár
We extend Levy's call-by-push-value (CBPV) analysis from simple to dependent type theory (DTT) in order to study the interaction between computational effects and dependent types.…
A Framework for Dependent Types and Effects
Matthijs Vákár
We generalise Levy's call-by-push-value (CBPV) to dependent type theory, to gain a better understanding of how to combine dependent types with effects. We define a dependently type…
Games for Dependent Types
Samson Abramsky, Radha Jagadeesan, Matthijs Vákár
We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free…
A Categorical Semantics for Linear Logical Frameworks
Matthijs Vákár
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear lo…
Syntax and Semantics of Linear Dependent Types
Matthijs Vákár
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear lo…