F*(프로그래밍 언어)

F* (programming language)
F*
Fstar-official-logo-2015.png
패러다임다중 패러다임: 기능적, 필수적
설계자마이크로소프트 리서치인리아[1]
안정적 해제
타이핑 규율종속, 추론, 정적, 강력
OSLinux, macOS, Windows
면허증아파치 라이선스 2.0
웹사이트www.fstar-lang.org
영향을 받은
Coq, Dafny, F#, Lean, OCaml, Standard ML

F*(F star로 발음됨)는 ML에서 영감을 받아 프로그램 검증을 목적으로 하는 기능 프로그래밍 언어다.그것의 유형 체계는 의존적인 유형, 단색 효과, 그리고 정교함을 포함한다.이를 통해 기능적 정확성과 보안 특성을 포함한 프로그램에 대한 정밀한 사양을 표현할 수 있다.F* 타입 체커는 시만텍 해결수동 증명의 조합을 통해 프로그램이 자신의 사양을 충족한다는 것을 증명하는 것을 목표로 한다.F*로 작성된 프로그램은 OCaml, F#, C로 번역하여 실행할 수 있다.이전 버전의 F*도 자바스크립트로 번역될 수 있다.

최신 버전의 F*는 전적으로 F*와 F#의 공통 서브셋으로 작성되며 OCamlF# 양쪽 모두에서 부트스트랩이 작성된다.오픈 소스(아파치 라이선스 2.0 이하)로 GitHub에서 활발하게 개발 중이다.[2]

참조

  1. ^ "Microsoft Research Inria Joint Centre". MSR-INRIA.
  2. ^ "FStarLang/FStar". GitHub.

원천

  • Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads for Free". 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
  • Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago (2016). "Dependent Types and Multi-Monadic Effects in F*". 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

외부 링크