#자기소개 를 해볼까요.
@ranolpRanol☆P 와 동일인입니다...만 해당 계정은 근시일 내에 살릴 계획이 없습니다.
@ranolp 계정은 프로그래밍 언어론/해커스펍 사용기 위주 계정입니다.
- 다시 말하자면 그 외 일상적인 내용은 트위터에서 이야기한다는 뜻입니다...
- TypeScript와 얼추 호환되면서 제정신인 타입 추론 규칙을 가진 언어를 만들려고 타입 이론을 공부하고 있습니다.
- 좀 많이 전에는 Bidirectional Typing (J. Dunfield, N. Krishnaswami)을 읽었었고,
- 독일에 있는 튀빙겐 대학 내에서 연구하는 대수적 효과 언어 Effekt도 간단히 살펴보았었습니다.
- 최근에는 힌들리-밀너-다마스 타입 추론 위에 얹은 부타입 확장을 살펴보고 있습니다.
- 캠브릿지 대학 연구인 MLsub (S. Dolan and A. Mycroft)...
- 을 단순화한 Simple-sub (L. Parreaux)을 시작으로 MLstruct, Ultimate Conditional Syntax 등 홍콩대 연구를 많이 보고 있습니다
- MLscript가 정말 흥미로운 언어에요 ReScript but more Kotlin처럼 생겼음
- 올해 들어서 An Infinitely Large Napkin으로 군론과 군의 작용, 위상수학과 대수 위상(호모토피만), 그리고 범주론을 배웠습니다.
- 형식적 증명 보조기에도 관심이 많습니다.
- Software Foundation을 통해 Coq (현 Rocq)를 약간 배웠습니다.
- Lean 4도 약간 맛보기를 했습니다.
- 의존 타입/마틴 뢰프 타입(MLTT)/호모토피 타입(HoTT) 등을 배워 간단한 증명 보조기도 만들어보고 싶네요.
- 아마 An Infinitely Large Napkin 스터디가 끝나면 HoTT 스터디를 하지 않을까 싶네요.
