F* swMATH ID: 27563 Software Authors: Microsoft Research, INRIA; Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean Description: 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. Homepage: https://www.fstar-lang.org/ Source Code: https://github.com/FStarLang/FStar Related Software: Coq; EasyCrypt; Nuprl; Idris; Irdis; z3; AURA; Zoo Probabilistic Systems; Lifting; Transfer; Autoref; Isabelle/HOL; Fable; JFlow; Why3; Links; JavaScript; ProVerif; Cayenne; Scribble Cited in: 20 Publications Further Publications: https://www.fstar-lang.org/#papers Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Secure distributed programming with value-dependent types. Zbl 1290.68033Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean 2013 Secure distributed programming with value-dependent types. Zbl 1323.68229Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean 2011 all top 5 Cited by 55 Authors 3 Bhargavan, Karthikeyan 3 Fournet, Cédric 3 Swamy, Nikhil 2 Barthe, Gilles 2 Caires, Luís 2 Chen, Juan 2 Dezani-Ciancaglini, Mariangiola 2 Lochbihler, Andreas 2 Strub, Pierre-Yves 2 Thiemann, Peter J. 2 Toninho, Bernardo 2 Yang, Jean 1 Ahman, Danel 1 Baillot, Patrick 1 Bartoletti, Massimo 1 Basin, David A. 1 Betarte, Gustavo 1 Bi, Xuan 1 Bugliesi, Michele 1 Calzavara, Stefano 1 Campo, Juan Diego 1 Castellani, Ilaria 1 Coppo, Mario 1 Dagand, Pierre-Evariste 1 Dal Lago, Ugo 1 Deniélou, Pierre-Malo 1 Fallah, Mehran S. 1 Focardi, Riccardo 1 Ghilezan, Silvia 1 Gordon, Andrew D. 1 Harris, William R. 1 Hriţcu, Cătălin 1 Jha, Somesh 1 Lepigre, Rodolphe 1 Lourenço, Luísa 1 Luna, Carlos 1 Maillard, Kenji 1 Martínez, Guido 1 McBride, Conor Thomas 1 Oliveira, Bruno C.d. S. 1 Padovani, Luca 1 Pantović, Jovanka 1 Pérez, Jorge A. 1 Pfenning, Frank 1 Pichardie, David 1 Plotkin, Gordon D. 1 Protzenko, Jonathan 1 Rastogi, Aseem 1 Reps, Thomas W. 1 Sattarzadeh, Behnam 1 Sefidgar, S. Reza 1 Seshia, Sanjit Arunkumar 1 Vieira, Hugo Torres 1 Yang, Yanpeng 1 Yoshida, Nobuko Cited in 5 Serials 3 Journal of Logical and Algebraic Methods in Programming 2 Journal of Automated Reasoning 2 Journal of Functional Programming 1 Journal of Cryptology 1 Formal Methods in System Design Cited in 4 Fields 20 Computer science (68-XX) 6 Information and communication theory, circuits (94-XX) 3 Mathematical logic and foundations (03-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year