5 Search Results for "Nanevski, Aleksandar"

Document
DOI: 10.4230/LIPIcs.FSCD.2025.4
Substructural Parametricity

Authors: C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.
Cite as

C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning. Substructural Parametricity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aberle_et_al:LIPIcs.FSCD.2025.4,
  author =	{Aberl\'{e}, C. B. and Crary, Karl and Martens, Chris and Pfenning, Frank},
  title =	{{Substructural Parametricity}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.4},
  URN =		{urn:nbn:de:0030-drops-236193},
  doi =		{10.4230/LIPIcs.FSCD.2025.4},
  annote =	{Keywords: Substructural type systems, logical relations, ordered logic}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.11
Formally Specifying Contract Optimizations with Bisimulations in Coq

Authors: Derek Sorensen

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
The efficacy of formal verification of smart contracts depends on being able to correctly specify and carry out the verification of optimized code. However, code optimized for performance is rarely optimized for intelligibility, which can make formally verifying optimized code difficult and costly. To address this issue, we present a formal tool for reasoning about an optimized contract in terms of its reference implementation. This tool reduces the work of formally verifying an optimized contract to proving behavioral equivalence to the reference implementation.
Cite as

Derek Sorensen. Formally Specifying Contract Optimizations with Bisimulations in Coq. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sorensen:OASIcs.FMBC.2025.11,
  author =	{Sorensen, Derek},
  title =	{{Formally Specifying Contract Optimizations with Bisimulations in Coq}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{11:1--11:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.11},
  URN =		{urn:nbn:de:0030-drops-230382},
  doi =		{10.4230/OASIcs.FMBC.2025.11},
  annote =	{Keywords: smart contract verification, formal methods, interactive theorem prover, smart contract upgradeability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.30
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack

Authors: Jesús Domínguez and Aleksandar Nanevski

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points (LP). However, LPs often hinder abstraction, and for some algorithms such as the timestamped stack, it is unclear how to even identify their LPs. In this paper, we show how to develop declarative proofs of linearizability by foregoing LPs and instead employing axiomatization of so-called visibility relations. While visibility relations have been considered before for the timestamped stack, our study is the first to show how to derive the axiomatization systematically and intuitively from the sequential specification of the stack. In addition to the visibility relation, a novel separability relation emerges to generalize real-time precedence of procedure invocation. The visibility and separability relations have natural definitions for the timestamped stack, and enable a novel proof that reduces the algorithm to a simplified form where the timestamps are generated atomically.
Cite as

Jesús Domínguez and Aleksandar Nanevski. Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dominguez_et_al:LIPIcs.CONCUR.2023.30,
  author =	{Dom{\'\i}nguez, Jes\'{u}s and Nanevski, Aleksandar},
  title =	{{Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.30},
  URN =		{urn:nbn:de:0030-drops-190245},
  doi =		{10.4230/LIPIcs.CONCUR.2023.30},
  annote =	{Keywords: Linearizability, Visibility Relations, Timestamped Stack}
}
Document
DOI: 10.4230/DARTS.3.2.4
Concurrent Data Structures Linked in Time (Artifact)

Authors: Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact provides the full mechanization in FCSL of the developments in the companion paper, "Concurrent Data Structures Linked in Time". In the latter, we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We illustrate the method by verifying (mechanically in FCSL) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients. FCSL is the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. It is implemented as an embedded domain-specific language (DSL) in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning.
Cite as

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{delbianco_et_al:DARTS.3.2.4,
  author =	{Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
  title =	{{Concurrent Data Structures Linked in Time (Artifact)}},
  pages =	{4:1--4:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.4},
  URN =		{urn:nbn:de:0030-drops-72850},
  doi =		{10.4230/DARTS.3.2.4},
  annote =	{Keywords: separation logic, linearization Points, concurrent snapshots, FCSL}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.8
Concurrent Data Structures Linked in Time

Authors: Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated. In this paper we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We name the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. We illustrate the method by verifying (mechanically in Coq) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients.
Cite as

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent Data Structures Linked in Time. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 8:1-8:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{delbianco_et_al:LIPIcs.ECOOP.2017.8,
  author =	{Delbianco, Germ\'{a}n Andr\'{e}s and Sergey, Ilya and Nanevski, Aleksandar and Banerjee, Anindya},
  title =	{{Concurrent Data Structures Linked in Time}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{8:1--8:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.8},
  URN =		{urn:nbn:de:0030-drops-72558},
  doi =		{10.4230/LIPIcs.ECOOP.2017.8},
  annote =	{Keywords: Separation logic, Linearization Points, Concurrent snapshots, FCSL}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2023
  • 2 2017

  • Refine by Author
  • 3 Nanevski, Aleksandar
  • 2 Banerjee, Anindya
  • 2 Delbianco, Germán Andrés
  • 2 Sergey, Ilya
  • 1 Aberlé, C. B.
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 1 OASIcs
  • 1 DARTS

  • Refine by Classification
  • 2 Theory of computation → Program verification
  • 1 Theory of computation → Type structures

  • Refine by Keyword
  • 2 FCSL
  • 1 Concurrent snapshots
  • 1 Linearizability
  • 1 Linearization Points
  • 1 Separation logic
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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