확장 ML

확장 ML은 ML을 기반으로 하는 광범위한 언어로 사양과 구현을 모두 포함합니다.ML의 구문을 확장하여 실행 가능하지는 않지만 프로그램의 동작을 엄격하게 지정할 수 있는 공리를 포함합니다.이 추가 기능으로 언어를 단계적 정교화에 사용할 수 있으며, 최초 공식 사양에서 점차적으로 진행되어 최종적으로 실행 가능한 표준 ML 프로그램을 생성할 수 있습니다.그 후, 원래의 사양에 대한 최종 실행 파일의 정확성은, 각 정제 스텝의 정확성을 증명하는 것으로 확립할 수 있다.확장 ML은 정식 프로그램 개발 및 사양에 대한 연구와 교육, 자동 프로그램 검증 연구에 사용됩니다.

확장 ML은 프로그래밍 언어 Extensible ML(ML에서 유사하게 파생된 것 제외)이나 사양 언어 Extensible Markup Language(XML)와는 관련이 없습니다.