Search Results

Documents authored by Wang, Qian

Found 2 Possible Name Variants:

Wang, Qian

Document
DOI: 10.4230/LIPIcs.CSL.2013.653
Semantics of Intensional Type Theory extended with Decidable Equational Theories

Authors: Qian Wang and Bruno Barras

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality generally leads to undecidable type-checking, it seems a reasonable trade-off to extend intensional equality with a decidable first-order theory, as experimented in earlier work on CoqMTU and its implementation CoqMT. In this work, CoqMTU is extended with strong eliminations. The meta-theoretical study, particularly the part relying on semantic arguments, is more complex. A set-theoretical model of the equational theory is the key ingredient to derive the logical consistency of the formalism. Strong normalization, the main lemma from which type-decidability follows, is proved by attaching realizability information to the values of the model. The approach we have followed is to first consider an abstract notion of first-order equational theory, and then instantiate it with a particular instance, Presburger Arithmetic. These results have been formalized using Coq.
Cite as

Qian Wang and Bruno Barras. Semantics of Intensional Type Theory extended with Decidable Equational Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 653-667, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.CSL.2013.653,
  author =	{Wang, Qian and Barras, Bruno},
  title =	{{Semantics of Intensional Type Theory extended with Decidable Equational Theories}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{653--667},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.653},
  URN =		{urn:nbn:de:0030-drops-42241},
  doi =		{10.4230/LIPIcs.CSL.2013.653},
  annote =	{Keywords: Calculus of Constructions, Extensional Type Theory, Intensional Type Theory, Model, Meta-theory, Consistency, Strong Normalization, Presburger Arithme}
}

Wang, Qiang

Document
DOI: 10.4230/LIPIcs.CONCUR.2016.30
Parameterized Systems in BIP: Design and Model Checking

Authors: Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems. Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.
Cite as

Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis. Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{konnov_et_al:LIPIcs.CONCUR.2016.30,
  author =	{Konnov, Igor and Kotek, Tomer and Wang, Qiang and Veith, Helmut and Bliudze, Simon and Joseph Sifakis},
  title =	{{Parameterized Systems in BIP: Design and Model Checking}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.30},
  URN =		{urn:nbn:de:0030-drops-61670},
  doi =		{10.4230/LIPIcs.CONCUR.2016.30},
  annote =	{Keywords: Rigorous system design, BIP, verification, parameterized model checking}
}
Document
DOI: 10.4230/LIPIcs.TQC.2013.192
Symmetries of Codeword Stabilized Quantum Codes

Authors: Salman Beigi, Jianxin Chen, Markus Grassl, Zhengfeng Ji, Qiang Wang, and Bei Zeng

Published in: LIPIcs, Volume 22, 8th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2013)

Abstract
Symmetry is at the heart of coding theory. Codes with symmetry, especially cyclic codes, play an essential role in both theory and practical applications of classical error-correcting codes. Here we examine symmetry properties for codeword stabilized (CWS) quantum codes, which is the most general framework for constructing quantum error-correcting codes known to date. A CWS code Q can be represented by a self-dual additive code S and a classical code C, i.e., Q=(S,C), however this representation is in general not unique. We show that for any CWS code Q with certain permutation symmetry, one can always find a self-dual additive code S with the same permutation symmetry as Q such that Q=(S,C). As many good CWS codes have been found by starting from a chosen S, this ensures that when trying to find CWS codes with certain permutation symmetry, the choice of S with the same symmetry will suffice. A key step for this result is a new canonical representation for CWS codes, which is given in terms of a unique decomposition as union stabilizer codes. For CWS codes, so far mainly the standard form (G,C) has been considered, where G is a graph state. We analyze the symmetry of the corresponding graph of G, which in general cannot possess the same permutation symmetry as Q. We show that it is indeed the case for the toric code on a square lattice with translational symmetry, even if its encoding graph can be chosen to be translational invariant.
Cite as

Salman Beigi, Jianxin Chen, Markus Grassl, Zhengfeng Ji, Qiang Wang, and Bei Zeng. Symmetries of Codeword Stabilized Quantum Codes. In 8th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 22, pp. 192-206, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{beigi_et_al:LIPIcs.TQC.2013.192,
  author =	{Beigi, Salman and Chen, Jianxin and Grassl, Markus and Ji, Zhengfeng and Wang, Qiang and Zeng, Bei},
  title =	{{Symmetries of Codeword Stabilized Quantum Codes}},
  booktitle =	{8th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2013)},
  pages =	{192--206},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-55-2},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{22},
  editor =	{Severini, Simone and Brandao, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2013.192},
  URN =		{urn:nbn:de:0030-drops-43129},
  doi =		{10.4230/LIPIcs.TQC.2013.192},
  annote =	{Keywords: CWS Codes, Union Stabilizer Codes, Permutation Symmetry, Toric Code}
}
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