Linear dependent types for differential privacy. (English) Zbl 1301.68111
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy, January 23–25, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1832-7). 357-370 (2013).
MSC:
| 68P15 | Database theory |
| 68N15 | Theory of programming languages |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Software:
z3References:
| [1] | M. S. Alvim, M. E. Andres, K. Chatzikokolakis, and C. Palamidessi. On the relation between Differential Privacy and Quantitative Information Flow. In Proc. ICALP, 2011. |
| [2] | G. Barthe and B. Köpf. Information-theoretic Bounds for Differentially Private Mechanisms. In Proc. CSF, 2011. 10.1109/CSF.2011.20 |
| [3] | G. Barthe, B. Kopf, F. Olmedo, and S. Zanella Beguelin. Probabilistic relational reasoning for differential privacy. In Proc. POPL, 2012. 10.1145/2103656.2103670 · Zbl 1321.68182 |
| [4] | A. Blum, C. Dwork, F. McSherry, and K. Nissim. Practical privacy: the SuLQ framework. In Proc. PODS, 2005. 10.1145/1065167.1065184 |
| [5] | K. Chaudhuri, C. Monteleoni, and A. D. Sarwate. Differentially private empirical risk minimization. J. Mach. Learn. Res., 12:1069-1109, July 2011. · Zbl 1280.62073 |
| [6] | S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. NavidPour. Proving programs robust. In Proc. FSE, 2011. 10.1145/2025113.2025131 |
| [7] | C. Chen and H. Xi. Combining programming with theorem proving. In Proc. ICFP, pages 66-77, 2005. 10.1145/1086365.1086375 · Zbl 1302.68241 |
| [8] | U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In IEEE LICS ’11, pages 133-142, 2011. 10.1109/LICS.2011.22 |
| [9] | U. Dal Lago and M. Hofmann. Bounded linear logic, revisited. In TLCA, volume 5608 of LNCS, pages 80-94. Springer, 2009. 10.1007/978-3-642-02273-9_8 · Zbl 1211.03089 |
| [10] | N. Dalvi, C. Ré, and D. Suciu. Probabilistic databases: diamonds in the dirt. Commun. ACM, 52(7):86-94, 2009. 10.1145/1538788.1538810 |
| [11] | L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. TACAS, 2008. |
| [12] | C. Dwork. Differential privacy. In Proc. ICALP, 2006. 10.1007/11787006_1 |
| [13] | C. Dwork, F. McSherry, K. Nissim, and A. Smith. Calibrating noise to sensitivity in private data analysis. In Proc. TCC, 2006. 10.1007/11681878_14 |
| [14] | M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy (extended version). http://privacy.cis.upenn.edu/papers/dfuzz-long.pdf. |
| [15] | J. Girard. Linear logic. Theor. Comp. Sci., 50(1):1-102, 1987. 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 |
| [16] | J. Girard, A. Scedrov, and P. Scott. Bounded linear logic. Theoretical Computer Science, 97(1):1-66, 1992. 10.1016/0304-3975(92)90386-T · Zbl 0788.03005 |
| [17] | T. J. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proc. PODS, 2007. 10.1145/1265530.1265535 |
| [18] | A. Gupta, K. Ligett, F. McSherry, A. Roth, and K. Talwar. Differentially private combinatorial optimization. In Proc. SODA, 2010. |
| [19] | A. Gupta, A. Roth, and J. Ullman. Iterative constructions and private data release. In Proc. TCC, 2012. 10.1007/978-3-642-28914-9_19 · Zbl 1304.68042 |
| [20] | A. Haeberlen, B. C. Pierce, and A. Narayan. Differential privacy under fire. In Proc. USENIX Security, 2011. |
| [21] | S. Hayashi. Singleton, union and intersection types for program extraction. In Proc. TACS, volume 526 of LNCS, pages 701-730. Springer Berlin / Heidelberg, 1991. · Zbl 1494.68059 |
| [22] | S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, and A. Smith. What can we learn privately? In Proc. FOCS, Oct. 2008. 10.1109/FOCS.2008.27 |
| [23] | N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In Proc. ICFP, 2012. 10.1145/2364527.2364536 |
| [24] | N. Li, T. Li, and S. Venkatasubramanian. t-closeness: Privacy beyond k-anonymity and l-diversity. In Proc. ICDE, 2007. |
| [25] | A. Machanavajjhala, D. Kifer, J. Abowd, J. Gehrke, and L. Vilhuber. Privacy: Theory meets practice on the map. In Proc. ICDE, 2008. 10.1109/ICDE.2008.4497436 |
| [26] | F. McSherry. Privacy integrated queries: an extensible platform for privacy-preserving data analysis. In Proc. SIGMOD, 2009. 10.1145/1559845.1559850 |
| [27] | F. McSherry and R. Mahajan. Differentially-private network trace analysis. In Proc. SIGCOMM, 2010. 10.1145/1851182.1851199 |
| [28] | F. McSherry and K. Talwar. Mechanism design via differential privacy. In Proc. FOCS, 2007. 10.1109/FOCS.2007.41 |
| [29] | P. Mohan, A. Thakurta, E. Shi, D. Song, and D. Culler. GUPT: privacy preserving data analysis made easy. In Proc. SIGMOD, 2012. 10.1145/2213836.2213876 |
| [30] | A. Narayanan and V. Shmatikov. Robust de-anonymization of large sparse datasets. In Proc. IEEE S&P, 2008. 10.1109/SP.2008.33 |
| [31] | C. Palamidessi and M. Stronati. Differential privacy for relational algebra: Improving the sensitivity bounds via constraint systems. In Proc. QAPLS, volume 85 of EPTCS, pages 92-105, 2012. · Zbl 1458.68062 |
| [32] | N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proc. POPL, 2002. 10.1145/503272.503288 |
| [33] | J. Reed, M. Gaboardi, and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy (extended version). http://privacy.cis.upenn.edu/papers/fuzz-long.pdf. |
| [34] | J. Reed and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In Proc. ICFP, Sept. 2010. 10.1145/1863543.1863568 |
| [35] | A. Roth and T. Roughgarden. The median mechanism: Interactive and efficient privacy with multiple queries. In Proc. STOC, 2010. |
| [36] | I. Roy, S. T. V. Setty, A. Kilzer, V. Shmatikov, and E.Witchel. Airavat: security and privacy for MapReduce. In Proc. NSDI, 2010. |
| [37] | D. Walker. Advanced Topics in Types and Programming Languages, chapter Substructural Type Systems. The MIT Press, 2005. |
| [38] | H. Xi and F. Pfenning. Dependent types in practical programming. In Proc. POPL, 1999. 10.1145/292540.292560 |
| [39] | L. Xu. Modular reasoning about differential privacy in a probabilistic process calculus. Manuscript, 2012. |
| [40] | B. A. Yorgey, S.Weirich, J. Cretin, S. Peyton Jones, D. Vytiniotis, and J. P. M. es. Giving Haskell a promotion. In Proc. TLDI, 2012. 10.1145/2103786.2103795 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
