45 citations · 398 across the 36 of their papers we have counts for
4 papers · 2 filters
Normalization by gluing for free λ-theories
Jonathan Sterling, Bas Spitters
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literatur…
Computer-aided proofs for multiparty computation with active security
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner +2
Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the…
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa +3
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked typ…
Internal Universes in Models of Homotopy Type Theory
Daniel R. Licata, Ian Orton, Andrew M. Pitts +1
We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties u…