Lean으로 하는 함수형 프로그래밍

 Lean으로 하는 함수형 프로그래밍🔗

David Thrane Christiansen

이 문서는 Functional Programming in Lean을 기계 번역 후 검토한 비공식 한국어 번역본이며, 원문과 마찬가지로 CC BY 4.0에 따라 이용할 수 있습니다. 한국어 번역이라는 변경 사항이 적용되었습니다.

Copyright Microsoft Corporation 2023 and Lean FRO, LLC 2023–2026

이 책은 Lean을 프로그래밍 언어로 사용하는 방법에 관한 무료 도서입니다. 모든 코드 샘플은 Lean 4.33.0 릴리스로 테스트되었습니다.

Contents

  1. 소개
  2. 감사의 글
  3. 1. Lean 알아가기
  4. 2. 안녕하세요, 세계!
  5. 막간: 명제, 증명, 그리고 인덱싱
  6. 3. 오버로딩과 타입 클래스
  7. 4. 모나드
  8. 5. 펑터, 애플리커티브 펑터, 모나드
  9. 6. 모나드 트랜스포머
  10. 7. 의존 타입을 사용한 프로그래밍
  11. 막간: 택틱, 귀납, 그리고 증명
  12. 8. 프로그래밍, 증명, 그리고 성능
  13. 9. 다음 단계