Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Kristina Sojakova"'
Publikováno v:
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. ⟨10.1145/3571223⟩
POPL 2023-50th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2023, Boston, United States. ⟨10.1145/3571223⟩
International audience; Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol at hand to be observationally equivalent to an idealized specification. While pervasive, formal tool supp
Publikováno v:
LICS
Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us
Autor:
Kristina Sojakova, Patricia Johann
Publikováno v:
LICS
Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3ebe15b6050f6b232a566c15f0aa794e
http://arxiv.org/abs/1805.00067
http://arxiv.org/abs/1805.00067
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 of a homotopy-initial algebra. This notion is defined by a purely type
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::acf03b1302f1d4081b557ad3dbf754a7
https://eprints.whiterose.ac.uk/105765/1/gambino-jacm.pdf
https://eprints.whiterose.ac.uk/105765/1/gambino-jacm.pdf
Autor:
Kristina Sojakova, Florian Rabe
Publikováno v:
ACM Transactions on Computational Logic. 14:1-34
Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an important r
Autor:
Kristina Sojakova
Homotopy type theory is a new branch of mathematics that merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic type-theoretic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e794dae4c04a5581615a8f983213ff45
Autor:
Mihai Codescu, Till Mossakowski, Kristina Sojakova, Florian Rabe, Michael Kohlhase, Fulya Horozal
Publikováno v:
Recent Trends in Algebraic Development Techniques ISBN: 9783642284113
WADT
WADT
LF is a meta-logical framework that has become a standard tool for representing logics and studying their properties. Its focus is proof theoretic, employing the Curry-Howard isomorphism: propositions are represented as types, and proofs as terms. He
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e93d00246f0e24d7261139c450c5a8a5
https://doi.org/10.1007/978-3-642-28412-0_10
https://doi.org/10.1007/978-3-642-28412-0_10
Publikováno v:
LICS
Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b58258e9847bac00b1e951d399e09c60
http://hdl.handle.net/10447/74875
http://hdl.handle.net/10447/74875
Publikováno v:
Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants.
We present a case study on a modular formal representation of algebra in the recently developed module system for the Twelf implementation of the Edinburgh Logical Framework LF. The module system employs signature morphisms as its main primitive conc
Autor:
Florian Rabe, Kristina Sojakova
Publikováno v:
Recent Trends in Algebraic Development Techniques ISBN: 9783642034282
WADT
WADT
DFOL is a logic that extends first-order logic with dependent types. We give a translation from DFOL to FOL formalized as an institution comorphism and show that it admits the model expansion property. This property together with the borrowing theore
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::79d7ef4b43d85cf4294dfe4adad877fb
https://doi.org/10.1007/978-3-642-03429-9_21
https://doi.org/10.1007/978-3-642-03429-9_21