The F* Project

Established: March 25, 2011

Publications

View by:

- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Download Project
- Verifying Higher-order Programs with the Dijkstra Monad
  
  Nikhil Swamy, Juan Chen, Ben Livshits
  
  ACM Programming Language Design and Implementation (PLDI) 2013 | June 2013
  
  ACM Programming Language Design and Implementation (PLDI) 2013
  
  Publication
- DKAL*: Constructing Executable Specifications of Authorization Protocols
  
  Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
  
  MSR-TR-2012-24 | March 2013
  
  International Symposium on Engineering Secure Software and Systems (ESSOS 13)
  
  Publication Publication
- Fully Abstract Compilation to JavaScript
  
  Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Ben Livshits
  
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013 | January 2013
  
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013
  
  Publication
- Verification Condition Generation with the Dijkstra State Monad
  
  Cole Schlesinger, Nikhil Swamy
  
  MSR-TR-2012-45 | April 2012
  
  Publication
- Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
  
  Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
  
  In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
  
  To appear
  
  Publication
- Secure Distributed Programming with Value-dependent Types
  
  Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
  
  The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) | September 2011
  
  Publication
- RePriv: Re-Envisioning In-Browser Privacy
  
  Matthew Fredrikson, Ben Livshits
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Publication
- Verified Security for Browser Extensions
  
  Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy, Ben Livshits
  
  Proceedings of the IEEE Symposium on Security and Privacy (Oakland) | May 2011
  
  Publication
- Secure Distributed Programming with Value-Dependent Types
  
  Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, Jean Yang
  
  MSR-TR-2011-37 | March 2011
  
  This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming.
  
  Publication
- Verifying Stateful Programs with Substructural State and Hoare Types
  
  Juan Chen, Nikhil Swamy
  
  Programming Language meets Program Verification (PLPV 2011) | January 2011
  
  Publication
- Type-preserving compilation for end-to-end verification of security enforcement
  
  Juan Chen, Nikhil Swamy, Ravi Chugh
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
  
  Publication
- Enforcing Stateful Authorization and Information Flow Policies in Fine
  
  Nikhil Swamy, Juan Chen, Ravi Chugh
  
  MSR-TR-2009-164 | March 2010
  
  ESOP 2010: 19th European Symposium on Programming
  
  Publication Publication

- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Download Project
- DKAL*: Constructing Executable Specifications of Authorization Protocols
  
  Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
  
  MSR-TR-2012-24 | March 2013
  
  International Symposium on Engineering Secure Software and Systems (ESSOS 13)
  
  Publication Publication
- Fully Abstract Compilation to JavaScript
  
  Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Ben Livshits
  
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013 | January 2013
  
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013
  
  Publication
- Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
  
  Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
  
  In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
  
  To appear
  
  Publication
- Secure Distributed Programming with Value-dependent Types
  
  Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
  
  The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) | September 2011
  
  Publication
- RePriv: Re-Envisioning In-Browser Privacy
  
  Matthew Fredrikson, Ben Livshits
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Publication
- Secure Distributed Programming with Value-Dependent Types
  
  Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, Jean Yang
  
  MSR-TR-2011-37 | March 2011
  
  This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming.
  
  Publication
- Verifying Stateful Programs with Substructural State and Hoare Types
  
  Juan Chen, Nikhil Swamy
  
  Programming Language meets Program Verification (PLPV 2011) | January 2011
  
  Publication
- Type-preserving compilation for end-to-end verification of security enforcement
  
  Juan Chen, Nikhil Swamy, Ravi Chugh
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
  
  Publication
- Enforcing Stateful Authorization and Information Flow Policies in Fine
  
  Nikhil Swamy, Juan Chen, Ravi Chugh
  
  MSR-TR-2009-164 | March 2010
  
  ESOP 2010: 19th European Symposium on Programming
  
  Publication Publication
- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Download Project
- Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
  
  Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
  
  In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
  
  To appear
  
  Publication
- Type-preserving compilation for end-to-end verification of security enforcement
  
  Juan Chen, Nikhil Swamy, Ravi Chugh
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
  
  Publication
- Verifying Higher-order Programs with the Dijkstra Monad
  
  Nikhil Swamy, Juan Chen, Ben Livshits
  
  ACM Programming Language Design and Implementation (PLDI) 2013 | June 2013
  
  ACM Programming Language Design and Implementation (PLDI) 2013
  
  Publication
- Verification Condition Generation with the Dijkstra State Monad
  
  Cole Schlesinger, Nikhil Swamy
  
  MSR-TR-2012-45 | April 2012
  
  Publication
- Verified Security for Browser Extensions
  
  Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy, Ben Livshits
  
  Proceedings of the IEEE Symposium on Security and Privacy (Oakland) | May 2011
  
  Publication
- Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
  
  Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
  
  In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
  
  To appear
  
  Publication
- Type-preserving compilation for end-to-end verification of security enforcement
  
  Juan Chen, Nikhil Swamy, Ravi Chugh
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
  
  Publication

- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Download Project
- Verifying Higher-order Programs with the Dijkstra Monad
  
  Nikhil Swamy, Juan Chen, Ben Livshits
  
  ACM Programming Language Design and Implementation (PLDI) 2013 | June 2013
  
  ACM Programming Language Design and Implementation (PLDI) 2013
  
  Publication
- Fully Abstract Compilation to JavaScript
  
  Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, Ben Livshits
  
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013 | January 2013
  
  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) 2013
  
  Publication
- Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq
  
  Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
  
  In Proceedings of the ACM Symposium on Principles on Programming Languages | January 2012
  
  To appear
  
  Publication
- Secure Distributed Programming with Value-dependent Types
  
  Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
  
  The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011) | September 2011
  
  Publication
- RePriv: Re-Envisioning In-Browser Privacy
  
  Matthew Fredrikson, Ben Livshits
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Publication
- Verified Security for Browser Extensions
  
  Arjun Guha, Matthew Fredrikson, Benjamin Livshits, Nikhil Swamy, Ben Livshits
  
  Proceedings of the IEEE Symposium on Security and Privacy (Oakland) | May 2011
  
  Publication
- Verifying Stateful Programs with Substructural State and Hoare Types
  
  Juan Chen, Nikhil Swamy
  
  Programming Language meets Program Verification (PLPV 2011) | January 2011
  
  Publication
- Type-preserving compilation for end-to-end verification of security enforcement
  
  Juan Chen, Nikhil Swamy, Ravi Chugh
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010 | June 2010
  
  ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) 2010
  
  Publication
- DKAL*: Constructing Executable Specifications of Authorization Protocols
  
  Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, Nikhil Swamy
  
  MSR-TR-2012-24 | March 2013
  
  International Symposium on Engineering Secure Software and Systems (ESSOS 13)
  
  Publication Publication
- Verification Condition Generation with the Dijkstra State Monad
  
  Cole Schlesinger, Nikhil Swamy
  
  MSR-TR-2012-45 | April 2012
  
  Publication
- Secure Distributed Programming with Value-Dependent Types
  
  Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, Jean Yang
  
  MSR-TR-2011-37 | March 2011
  
  This is an extended version of the conference paper (ICFP '11) with the same title. A final version of this full technical report is forthcoming.
  
  Publication
- Enforcing Stateful Authorization and Information Flow Policies in Fine
  
  Nikhil Swamy, Juan Chen, Ravi Chugh
  
  MSR-TR-2009-164 | March 2010
  
  ESOP 2010: 19th European Symposium on Programming
  
  Publication Publication

People

Cédric Fournet

Senior Principal Research Manager

Learn more

Nikhil Swamy

Senior Principal Researcher

Learn more

Santiago Zanella-Béguelin

Principal Researcher

Learn more