Search Results

Documents authored by Wang, Yuting

Document
DOI: 10.4230/LIPIcs.ECOOP.2026.21
Foundational and Compositional Verification of Layered Concurrent Objects

Authors: Yicheng Ni and Yuting Wang

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
Compositionality is essential for managing complexity in verification of concurrent programs, especially when proof certificates are needed. An effective verification scheme is to divide programs into abstraction layers and verify by composing refinements between layers. However, vanilla verified layers come with global states which severely limit their extensibility. This problem may be solved by dividing a layer into objects with encapsulated local states. Although the idea has been successfully realized in the sequential setting, it remains unclear if it also works in a concurrent setting where function calls across layers are no longer atomic steps and foundational proofs are needed. We propose an approach to foundational and compositional verification of concurrent objects organized into multiple layers. The central idea is to represent concurrent objects as open labeled transition systems with encapsulated threads and to adopt trace refinements as a uniform notion of functional correctness which supports both vertical composition (layered refinement) and horizontal composition (extension of layer interfaces). Due to the operational nature of transition systems, it is straightforward to adopt traditional simulation techniques to produce foundational proof certificates. We implement this framework in the Rocq theorem prover and demonstrate its capability in foundational and compositional verification by verifying non-trivial lock-free concurrent data structures.
Cite as

Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 21:1-21:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ni_et_al:LIPIcs.ECOOP.2026.21,
  author =	{Ni, Yicheng and Wang, Yuting},
  title =	{{Foundational and Compositional Verification of Layered Concurrent Objects}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{21:1--21:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.21},
  URN =		{urn:nbn:de:0030-drops-261171},
  doi =		{10.4230/LIPIcs.ECOOP.2026.21},
  annote =	{Keywords: Concurrency, Compositional Verification}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.16
Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)

Authors: Yicheng Ni and Yuting Wang

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This document provides artifact description for the ECOOP 2026 paper "Foundational and Compositional Verification of Layered Concurrent Objects".
Cite as

Yicheng Ni and Yuting Wang. Foundational and Compositional Verification of Layered Concurrent Objects (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{ni_et_al:DARTS.12.1.16,
  author =	{Ni, Yicheng and Wang, Yuting},
  title =	{{Foundational and Compositional Verification of Layered Concurrent Objects (Artifact)}},
  pages =	{16:1--16:11},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Ni, Yicheng and Wang, Yuting},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.16},
  URN =		{urn:nbn:de:0030-drops-261531},
  doi =		{10.4230/DARTS.12.1.16},
  annote =	{Keywords: Formal Verification, Concurrency, Formalization, Rocq}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.332
A Proof-theoretic Characterization of Independence in Type Theory

Authors: Yuting Wang and Kaustuv Chaudhuri

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
For lambda-terms constructed freely from a type signature in a type theory such as LF, there is a simple inductive subordination relation that is used to control type-formation. There is a related—but not precisely complementary—notion of independence that asserts that the inhabitants of the function space tau_1 --> tau_2 depend vacuously on their arguments. Independence has many practical reasoning applications in logical frameworks, such as pruning variable dependencies or transporting theorems and proofs between type signatures. However, independence is usually not given a formal interpretation. Instead, it is generally implemented in an ad hoc and uncertified fashion. We propose a formal definition of independence and give a proof-theoretic characterization of it by: (1) representing the inference rules of a given type theory and a closed type signature as a theory of intuitionistic predicate logic, (2) showing that typing derivations in this signature are adequately represented by a focused sequent calculus for this logic, and (3) defining independence in terms of strengthening for intuitionistic sequents. This scheme is then formalized in a meta-logic, called G, that can represent the sequent calculus as an inductive definition, so the relevant strengthening lemmas can be given explicit inductive proofs. We present an algorithm for automatically deriving the strengthening lemmas and their proofs in G.
Cite as

Yuting Wang and Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 332-346, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.TLCA.2015.332,
  author =	{Wang, Yuting and Chaudhuri, Kaustuv},
  title =	{{A Proof-theoretic Characterization of Independence in Type Theory}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{332--346},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.332},
  URN =		{urn:nbn:de:0030-drops-51736},
  doi =		{10.4230/LIPIcs.TLCA.2015.332},
  annote =	{Keywords: subordination; independence; sequent calculus; focusing; strengthening}
}
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact