Author name cluster

Matthijs Vákár

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

I&C Journal 2018 Journal Article

Game semantics for dependent types

Matthijs Vákár
Radha Jagadeesan
Samson Abramsky

We present a model of dependent type theory (DTT) with Π-, 1-, Σ- and intensional Id -types, which is based on a slight variation of the (call-by-name) category of AJM-games and history-free winning well-bracketed strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. We show it contains a submodel as a full subcategory which gives a faithful interpretation of DTT with Π-, 1-, Σ- and intensional Id -types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id -types, as well as at the more general class of types where we allow for one strictly positive occurrence of an Id -type. Definability for the full type hierarchy with Id -types remains to be investigated.

Details DOI

UAI Conference 2017 Conference Paper

Interpreting Lion Behaviour as Probabilistic Programs

Neil Dhir
Matthijs Vákár
Matthew Wijers
Andrew Markham
Frank Wood

We consider the problem of unsupervised learning of meaningful behavioural segments of high-dimensional time-series observations, collected from a pride of African lions1. We demonstrate, by way of a probabilistic programming system (PPS), a methodology which allows for quick iteration over models and Bayesian inferences, which enables us to learn meaningful behavioural segments. We introduce a new Bayesian nonparametric (BNP) state-space model, which extends the hierarchical Dirichlet process (HDP) hidden Markov model (HMM) with an explicit BNP treatment of duration distributions, to deal with different levels of granularity of the latent behavioural space of the lions. The ease with which this is done exemplifies the flexibility that a PPS gives a scientist2. Furthermore, we combine this approach with unsupervised feature learning, using variational autoencoders.

Details