유형 검사기 라이브러리

Question

저는 컴파일러를 찾고 있습니다. 유형 검사를 수행 할 수있는 라이브러리를 찾고 있습니다. 지금까지 아무 것도 찾지 못했습니다 =/좋은 타입 검사 라이브러리를 아십니까? 하스켈을 사용하고 있지만 라이브러리가 좋다면 다른 언어도 고려해 보겠습니다.)

Answer 1

형식 검사기의 비트를 돕는 라이브러리가있을 수 있습니다. 특히 형식 검사기가 필요하고 형식 유추가 필요하지 않은 경우 특히 그렇습니다. 예를 들어, 하스켈에 논리 프로그래밍을 내장 한 라이브러리가 있습니다. 10,000 피트에서 논리 프로그래밍을 사용하여 유형 프로그래밍을 사용하는 것이 더 쉽습니다 (예 : shaper으로 언급 된 카멜레온은 포함 된 CHR 언어를 기반으로합니다. 하스켈).

하스켈의 임베디드 로직 프로그래밍은 전에 유형 검사기를 작성한 적이 없다면 거의 문서화되지 않은 큰 단계입니다. 마찬가지로 속성 문법 (예 : UUAG)은 글쓰기에 필요한 기계류를 제공하는 유쾌한 형식주의이지만 이전에 사용한 적이없는 푯말이 적은 장소에 배치 할 수 있습니다.

전에 유형 검사기를 작성하지 않았다면 라이브러리에 대해 걱정하지 않고 처음부터 프로세스를 진행하는 것이 더 나을 것입니다. 마크 P. 존스 (Mark P. Jones)의 "하스켈에서 타이핑 하스켈 (Haskell in Typing Haskell)"논문은 아마 그 어떤 출발점처럼 좋은 출발점 일 것이다.

Answer 2

아마 Martin Sulzmann의 Chameleon이 도움이 될까요?

Answer 3

dedukti, hybrid 및 lambdacube을 포함하여 여러 유형의 체커가 발견되었습니다.이 중 하나가 작동 할 가능성이 있습니까?