F*(프로그래밍 언어)

F*

패러다임	다중 패러다임: 기능적, 필수적
설계자	마이크로소프트 리서치 앤 인리아[1]
안정적 해제	리포지토리
타이핑 규율	종속, 추론, 정적, 강력
OS	Linux, 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#의 공통 서브셋으로 작성되며 OCaml과 F# 양쪽 모두에서 부트스트랩이 작성된다.오픈 소스(아파치 라이선스 2.0 이하)로 GitHub에서 활발하게 개발 중이다.^[2]

참조

원천

• 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.

외부 링크

• F* 홈페이지
• GitHub의 F* 소스 코드
• F* 자습서

이 프로그래밍 언어 관련 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.

• v
• t