F*
1. 개요
F*는 함수형 프로그래밍 언어이다. 2022년 3월 24일 버전까지 F*는 F*와 F#의 공통 하위 집합으로 작성되었으며, OCaml과 F# 모두에서 부트스트래핑을 지원했으나, 2022년 4월 2일 버전부터 이 방식은 중단되었다. F*는 일반적인 산술 연산자와 관계 연산자를 지원하며, bool, int, float, char, unit과 같은 원시 자료형을 제공한다. 관련 연구로 Ahman 외(2017)는 Dijkstra Monads for Free를 발표했으며, Swamy 외(2016)는 F*의 종속 타입 및 다중 모나드 효과를 발표했다.
이미지 준비중입니다.
| 개발자 | 마이크로소프트 리서치, Inria |
|---|---|
| 출시일 | 2011년 |
| 최신 버전 | v2023.09.03 |
| 최신 버전 출시일 | 2023년 9월 3일 |
| 종류 | 다중 패러다임: 함수형 프로그래밍, 명령형 프로그래밍 |
| 계열 | ML: Caml: OCaml |
| 타이핑 | 종속, 추론, 정적, 강한 |
| 운영체제 | 크로스 플랫폼: 리눅스, macOS, 윈도우 |
| 라이선스 | Apache 2.0 |
| 웹사이트 | F* 공식 웹사이트 |
| 파일 확장자 | .fst |
| 영향 받은 언어 | Coq, Dafny, F#, Lean, OCaml, Standard ML |
| 설계자 | Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang |
-
2013년 개발된 프로그래밍 언어 -
퓨어스크립트
퓨어스크립트는 2013년 필 프리먼이 설계한 함수형 프로그래밍 언어이며, 하스켈과 유사한 타입 시스템을 갖추고 자바스크립트 등으로 컴파일되며 엄격한 평가, 불변 자료 구조, 타입 추론을 특징으로 한다. -
2013년 개발된 프로그래밍 언어 -
엔트리 (프로그래밍 언어)
엔트리는 네이버 커넥트재단에서 개발한 블록형 프로그래밍 교육 플랫폼으로, 블록 조립을 통해 프로그래밍 학습, 창작물 제작 및 공유가 가능하며, 한국어 지원과 교육 환경에 최적화된 기능이 특징이다. -
ML 프로그래밍 언어 계열 -
OCaml
OCaml은 ML 계열의 함수형 프로그래밍 언어로서 클래스 기반 객체 지향 프로그래밍 기능을 지원하며, 강력한 타입 시스템, 타입 추론, 꼬리 재귀 최적화 등의 특징을 가진다. -
ML 프로그래밍 언어 계열 -
ML (프로그래밍 언어)
ML은 1970년대 초에 개발된 프로그래밍 언어로, 강력한 타입 시스템, 일급 함수, 가비지 컬렉션, 정적 타이핑 등의 기능을 제공하며 다양한 분야에서 활용된다. -
마이크로소프트 리서치 -
마이크로소프트 코그니티브 툴킷
-
마이크로소프트 리서치 -
Cω
2.1. 버전
2022년 3월 24일 버전까지 F*는 F*와 F#의 공통 하위 집합으로 작성되었으며, OCaml과 F# 모두에서 부트스트래핑을 지원했다. 2022년 4월 2일 버전부터 이 방식은 중단되었다.
3. 특징
F*는 마이크로소프트에서 개발한 함수형 프로그래밍 언어로, 프로그램 검증을 목표로 한다. F*는 ML과 유사한 문법을 가지고 있으며, 하스켈과 OCaml의 영향을 받았다. F*는 반결정적인 SMT 문제를 해결하기 위해 의존 타입, 모나딕 효과, 정제 타입과 같은 기능을 제공한다. F*는 타입 추론을 지원하며, 프로그래머가 명시적으로 타입을 지정하지 않아도 컴파일러가 타입을 유추할 수 있다.
3.1. 연산자
F*는 +, -, *, / 와 같은 일반적인 산술 연산자를 지원한다. 또한 F*는 <, <=, ==, !=, >, >= 와 같은 관계 연산자도 지원한다.