6 citations · 11 across the 6 of their papers we have counts for
9 papers
Concrete Security Bounds for Simulation-Based Proofs of Multi-Party Computation Protocols
Kristina Sojakova, Mihai Codescu, Joshua Gancher
The concrete security paradigm aims to give precise bounds on the probability that an adversary can subvert a cryptographic mechanism. This is in contrast to asymptotic security, w…
Money grows on (proof-)trees: the formal FA1.2 ledger standard
Murdoch Gabbay, Arvid Jakobsson, Kristina Sojakova
Once you have invented digital money, you may need a ledger to track who owns what -- and an interface to that ledger so that users of your money can transact. On the Tezos blockch…
Syllepsis in Homotopy Type Theory
Kristina Sojakova
It is well-known that in homotopy type theory (HoTT), one can prove the Eckmann-Hilton theorem: given two 2-loops p, q : 1 = 1 on the reflexivity path at an arbitrary point a : A,…
A General Framework for Relational Parametricity
Kristina Sojakova, Patricia Johann
Reynolds' original theory of relational parametricity was intended to capture the idea that polymorphically typed System F programs preserve all relations between inputs. But as Re…
Cubical Categories for Higher-Dimensional Parametricity
Patricia Johann, Kristina Sojakova
Reynolds' theory of relational parametricity formalizes parametric polymorphism for System F, thus capturing the idea that polymorphically typed System F programs always map relate…
The equivalence of the torus and the product of two circles in homotopy type theory
Kristina Sojakova
Homotopy type theory is a new branch of mathematics which merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us…
Homotopy-initial algebras in type theory
Steve Awodey, Nicola Gambino, Kristina Sojakova
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion…
Higher Inductive Types as Homotopy-Initial Algebras
Kristina Sojakova
Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We…
Inductive types in homotopy type theory
Steve Awodey, Nicola Gambino, Kristina Sojakova
Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebrai…