Recent papers

  • ITL+: a temporal programming model with atomic blocks.
    • Xiaoxiao Yang, Yu Zhang, Xinyu Feng, Ming Fu.
    Technical report ISCAS-SKLCS-11-18, Laboratory for Computer Science, ISCAS.
  • Program Equivalence in Linear Contexts.
    • Yuxin Deng, Yu Zhang.
    Technical report ISCAS-SKLCS-11-04, Laboratory for Computer Science, ISCAS.

    Papers

    Security protocols and formal cryptography:
  • A calculus for game-based security proofs.
    • David Nowak, Yu Zhang.
    In International Conference on Provable Security (ProvSec'2010), vol. 6402 of LNCS, October 2010.
    The draft is available at Cryptology ePrint Archive.
  • The computational SLR: a logic for reasoning about computational indistinguishability.
    • Yu Zhang.
    In Mathematical Structures in Computer Science, volume 20, issue 05, pp. 951-975, Cambridge University Press 2010.
    A short version was published in International Conference on Typed Lambda Calculi and Applications (TLCA'2009), vol. 5608 of LNCS, 2009.
  • Verifying anonymous credential systems in applied pi calculus.
    • Xiangxi Li, Yu Zhang, Yuxin Deng.
    In International Conference in Cryptology and Network Security (CANS'2009), vol. 5888 of LNCS, 2009.
  • An Open Framework for Remote Electronic Elections.
    • Yu Zhang.
    In International Conference in Cryptology and Network Security (CANS'2008), vol. 5339 of LNCS, 2008.
  • Cryptographic Logical Relations.
    • Yu Zhang.
    In Theoretical Computer Science, vol. 394/1-2, pp 39-63, March 2008.
  • Cryptographic Logical Relations.
    •        --- What is the contextual equivalence for cryptographic protocols and how to prove it?
    Yu Zhang.
    Ph.D. dissertation, ENS de Cachan, October 2005.
      Logic, theory of programming languages, type systems:
  • Program Equivalence in Linear Contexts.
    • Yuxin Deng, Yu Zhang.
    Technical report ISCAS-SKLCS-11-04, Laboratory for Computer Science, ISCAS.
  • On Completeness of Logical Relations for Monadic Types.
    • Slawomir Lasota, David Nowak, Yu Zhang.
    In Advances in Computer Science (ASIAN'06), vol. 4435 of LNCS, 2008. (long version)
  • Complete Lax Logical Relations for Cryptographic Lambda-Calculi.
    • Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, Yu Zhang.
    In International Conference of Computer Science Logic (CSL'04), vol. 3210 of LNCS, 2004.
  • Logical Relations for Dynamic Name Creation.
    • Yu Zhang, David Nowak.
    In International Conference of Computer Science Logic (CSL'03), vol. 2803 of LNCS, 2003.
      Formal verification of computer systems:
  • SystemC waiting-state automata.
    • Yu Zhang, Bruno Monsuez, Franck Védrine.
    In International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'07), 2007.