Search Results

Documents authored by Soloviev, Sergei

Document
DOI: 10.4230/LIPIcs.TYPES.2016.14
A Formal Study of Boolean Games with Random Formulas as Payoff Functions

Authors: Érik Martin-Dorel and Sergei Soloviev

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
In this paper, we present a probabilistic analysis of Boolean games. We consider the class of Boolean games where payoff functions are given by random Boolean formulas. This permits to study certain properties of this class in its totality, such as the probability of existence of a winning strategy, including its asymptotic behaviour. With the help of the Coq proof assistant, we develop a Coq library of Boolean games, to provide a formal proof of our results, and a basis for further developments.
Cite as

Érik Martin-Dorel and Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{martindorel_et_al:LIPIcs.TYPES.2016.14,
  author =	{Martin-Dorel, \'{E}rik and Soloviev, Sergei},
  title =	{{A Formal Study of Boolean Games with Random Formulas as Payoff Functions}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{14:1--14:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.14},
  URN =		{urn:nbn:de:0030-drops-98486},
  doi =		{10.4230/LIPIcs.TYPES.2016.14},
  annote =	{Keywords: Boolean games, Random process, Coq formal proofs}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.274
On Isomorphism of Dependent Products in a Typed Logical Framework

Authors: Sergei Soloviev

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
A complete decision procedure for isomorphism of kinds that contain only dependent product, constant Type and variables is obtained. All proofs are done using Z. Luo's logical framework. They can be easily transferred to a large class of type theories with dependent product.
Cite as

Sergei Soloviev. On Isomorphism of Dependent Products in a Typed Logical Framework. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 274-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{soloviev:LIPIcs.TYPES.2014.274,
  author =	{Soloviev, Sergei},
  title =	{{On Isomorphism of Dependent Products in a Typed Logical Framework}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{274--287},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.274},
  URN =		{urn:nbn:de:0030-drops-55013},
  doi =		{10.4230/LIPIcs.TYPES.2014.274},
  annote =	{Keywords: Isomorphism of types, dependent product, logical framework}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact