{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:45Z","timestamp":1779836745097,"version":"3.53.1"},"reference-count":57,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T00:00:00Z","timestamp":1383004800000},"content-version":"unspecified","delay-in-days":120,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Our language provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F*. We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. We have programmed and verified nearly 50,000 lines of F* including new schemes for multi-party sessions; a zero-knowledge privacy-preserving payment protocol; a provenance-aware curated database; a suite of web-browser extensions verified for authorization properties; a cloud-hosted multi-tier web application with a verified reference monitor; the core F* typechecker itself; and programs translated to F* from other languages such as F7 and JavaScript.<\/jats:p>","DOI":"10.1017\/s0956796813000142","type":"journal-article","created":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T10:36:59Z","timestamp":1383043019000},"page":"402-451","source":"Crossref","is-referenced-by-count":30,"title":["Secure distributed programming with value-dependent types"],"prefix":"10.1017","volume":"23","author":[{"given":"NIKHIL","family":"SWAMY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JUAN","family":"CHEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00c9DRIC","family":"FOURNET","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"PIERRE-YVES","family":"STRUB","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KARTHIKEYAN","family":"BHARGAVAN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JEAN","family":"YANG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,10,29]]},"reference":[{"key":"S0956796813000142_ref54","first-page":"369","volume-title":"Security and Privacy","author":"Swamy","year":"2008"},{"key":"S0956796813000142_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"S0956796813000142_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_16"},{"key":"S0956796813000142_ref45","volume-title":"Privacy-Friendly Smart Metering","author":"Rial","year":"2010"},{"key":"S0956796813000142_ref44","first-page":"129","volume-title":"Advances in Cryptology","author":"Pedersen","year":"1992"},{"key":"S0956796813000142_ref41","unstructured":"Mendler N. P. (1987) Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY."},{"key":"S0956796813000142_ref40","first-page":"21","volume-title":"IFIP Congress","author":"McCarthy","year":"1962"},{"key":"S0956796813000142_ref47","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"S0956796813000142_ref39","first-page":"3","volume-title":"Programming Languages Meets Program Verification","author":"Lahiri","year":"2011"},{"key":"S0956796813000142_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-912-1_14"},{"key":"S0956796813000142_ref35","first-page":"27","volume-title":"International Conference on Functional Programming","author":"Jia","year":"2008"},{"key":"S0956796813000142_ref56","first-page":"177","volume-title":"Computer Security Foundations Symposium","author":"Vaughan","year":"2008"},{"key":"S0956796813000142_ref33","first-page":"273","volume-title":"Principles of Programming Languages","author":"Honda","year":"2008"},{"key":"S0956796813000142_ref31","first-page":"149","volume-title":"Computer Security Foundations Symposium","author":"Gurevich","year":"2008"},{"key":"S0956796813000142_ref29","first-page":"115","volume-title":"Security and Privacy","author":"Guha","year":"2011"},{"key":"S0956796813000142_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"S0956796813000142_ref27","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2003-11402"},{"key":"S0956796813000142_ref26","volume-title":"A Small Scale Reflection Extension for the Coq System","author":"Gonthier","year":"2011"},{"key":"S0956796813000142_ref53","first-page":"266","volume-title":"International Conference on Functional Programming","author":"Swamy","year":"2011"},{"key":"S0956796813000142_ref36","first-page":"17","volume-title":"Programming Languages and Analysis for Security","author":"Jia","year":"2009"},{"key":"S0956796813000142_ref5","volume-title":"Probabilistic Relational Verification for Cryptographic Implementations","author":"Barthe","year":"2012"},{"key":"S0956796813000142_ref10","first-page":"445","volume-title":"Symposium on Principles of Programming Languages","author":"Bhargavan","year":"2010"},{"key":"S0956796813000142_ref43","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers Institute of Technology, Goteborg."},{"key":"S0956796813000142_ref18","first-page":"435","volume-title":"Symposium on Principles of Programming Languages","author":"Deni\u00e9lou","year":"2011"},{"key":"S0956796813000142_ref50","first-page":"571","volume-title":"Principles of Programming Languages","author":"Strub","year":"2012"},{"key":"S0956796813000142_ref37","first-page":"15","volume-title":"Programming Languages Meets Program Verification","author":"Kimmell","year":"2012"},{"key":"S0956796813000142_ref32","first-page":"168","volume-title":"European Symposium on Research in Computer Security","author":"Guts","year":"2009"},{"key":"S0956796813000142_ref11","first-page":"15","volume-title":"Programming Languages Meets Program Verification","author":"Borgstrom","year":"2011"},{"key":"S0956796813000142_ref12","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"S0956796813000142_ref57","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"S0956796813000142_ref46","volume-title":"Verification Condition Generation with the Dijkstra State Monad","author":"Schlesinger","year":"2012"},{"key":"S0956796813000142_ref25","unstructured":"Girard J.-Y. (1972) Interpr\u00e9;tation Fonctionelle et \u00e9;limination des Coupures de l'arithm\u00e9;tique d'ordre sup\u00e9;rieur. PhD thesis, Universit\u00e9; Paris VII, Paris."},{"key":"S0956796813000142_ref51","first-page":"49","volume-title":"Programming Languages Meets Program Verification","author":"Stump","year":"2008"},{"key":"S0956796813000142_ref30","first-page":"126","volume-title":"European Conference on Object-Oriented Programming","author":"Guha","year":"2010"},{"key":"S0956796813000142_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36563-8_10"},{"key":"S0956796813000142_ref21","first-page":"125","volume-title":"European Symposium on Programming","author":"Filli\u00e2tre","year":"2013"},{"key":"S0956796813000142_ref55","first-page":"387","volume-title":"Programming Languages Design and Implementation","author":"Swamy","year":"2013"},{"key":"S0956796813000142_ref42","first-page":"229","volume-title":"International Conference on Functional Programming","author":"Nanevski","year":"2008"},{"key":"S0956796813000142_ref1","first-page":"239","volume-title":"International Conference on Functional Programming","author":"Augustsson","year":"1998"},{"key":"S0956796813000142_ref52","first-page":"529","volume-title":"European Symposium on Programming","author":"Swamy","year":"2010"},{"key":"S0956796813000142_ref14","first-page":"412","volume-title":"Programming Language Design and Implementation","author":"Chen","year":"2010"},{"key":"S0956796813000142_ref19","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"S0956796813000142_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"S0956796813000142_ref2","first-page":"27","volume-title":"Types in Language Design and Implementation","author":"Avijit","year":"2010"},{"key":"S0956796813000142_ref3","first-page":"357","volume-title":"Computer and Communications Security","author":"Backes","year":"2008"},{"key":"S0956796813000142_ref4","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1992"},{"key":"S0956796813000142_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_18"},{"key":"S0956796813000142_ref7","first-page":"17","volume-title":"Computer Security Foundations Symposium","author":"Bengtson","year":"2008"},{"key":"S0956796813000142_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0956796813000142_ref9","first-page":"124","volume-title":"Computer Security Foundations Symposium","author":"Bhargavan","year":"2009"},{"key":"S0956796813000142_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1380584.1380587"},{"key":"S0956796813000142_ref15","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"S0956796813000142_ref23","first-page":"341","volume-title":"Computer and Communications Security","author":"Fournet","year":"2011"},{"key":"S0956796813000142_ref16","volume-title":"Chapter 4: Calculus of Inductive Constructions","year":"2010"},{"key":"S0956796813000142_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"S0956796813000142_ref22","first-page":"31","volume-title":"Computer Security Foundations Symposium","author":"Fournet","year":"2007"},{"key":"S0956796813000142_ref24","first-page":"371","volume-title":"Symposium on Principles of Programming Languages","author":"Fournet","year":"2013"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796813000142","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:30Z","timestamp":1779834990000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796813000142\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S0956796813000142"],"URL":"https:\/\/doi.org\/10.1017\/s0956796813000142","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}