F*

F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives. F*’s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.


References in zbMATH (referenced in 16 articles , 2 standard articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil: Dijkstra monads for free (2017)
  2. Bugliesi, Michele; Calzavara, Stefano; Focardi, Riccardo: Formal methods for web security (2017)
  3. Harris, William R.; Jha, Somesh; Reps, Thomas W.; Seshia, Sanjit A.: Program synthesis for interactive-security systems (2017)
  4. Lepigre, Rodolphe: A classical realizability model for a semantical value restriction (2016)
  5. Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
  6. McBride, Conor: I got plenty o’ nuttin’ (2016)
  7. Thiemann, Peter: A delta for hybrid type checking (2016)
  8. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
  9. Bartoletti, Massimo; Castellani, Ilaria; Deniélou, Pierre-Malo; Dezani-Ciancaglini, Mariangiola; Ghilezan, Silvia; Pantovic, Jovanka; Pérez, Jorge A.; Thiemann, Peter; Toninho, Bernardo; Vieira, Hugo Torres: Combining behavioural types with security analysis (2015)
  10. Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Padovani, Luca; Yoshida, Nobuko: A gentle introduction to multiparty asynchronous session types (2015)
  11. Sattarzadeh, Behnam; Fallah, Mehran S.: Automated type-based analysis of injective agreement in the presence of compromised principals (2015)
  12. Lourenço, Luísa; Caires, Luís: Information flow analysis for valued-indexed data security compartments (2014)
  13. Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2013)
  14. Fournet, Cédric; Bhargavan, Karthikeyan; Gordon, Andrew D.: Cryptographic verification by typing for a sample protocol implementation (2011)
  15. Pfenning, Frank; Caires, Luis; Toninho, Bernardo: Proof-carrying code in a session-typed process calculus (2011)
  16. Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2011)


Further publications can be found at: https://www.fstar-lang.org/#papers