Home >

news Help

Publication Information


Title
Japanese:Approximate Relational Hoare Logic for Continuous Random Samplings 
English:Approximate Relational Hoare Logic for Continuous Random Samplings 
Author
Japanese: 佐藤哲也.  
English: Tetsuya Sato.  
Language English 
Journal/Book name
Japanese:Electronic Notes in Theoretical Computer Science 
English:Electronic Notes in Theoretical Computer Science 
Volume, Number, Page Volume 325        Page 277-298
Published date Oct. 5, 2016 
Publisher
Japanese: 
English:Elsevier B.V. 
Conference name
Japanese: 
English: 
Conference site
Japanese: 
English: 
Official URL https://www.sciencedirect.com/science/article/pii/S1571066116300949
 
DOI https://doi.org/10.1016/j.entcs.2016.09.043
Abstract Approximate relational Hoare logic (apRHL) is a logic for formal verification of the differential privacy of databases written in the programming language pWHILE. Strictly speaking, however, this logic deals only with discrete random samplings. In this paper, we define the graded relational lifting of the subprobabilistic variant of Giry monad, which described differential privacy. We extend the logic apRHL with this graded lifting to deal with continuous random samplings. We give a generic method to give proof rules of apRHL for continuous random samplings.

©2007 Tokyo Institute of Technology All rights reserved.