Speaker:Mino Bai
Time:1999-01-26 ~ 1999-03
Place:Rm.2443 KAIST/CS

Abstract

CC(Calculus of Construction) 은 간단한 타입이론과 dependent 타입에 근거하고 있다. CC를 이용하여 논리의 모든 연산을 구현할 수도 있다. CC는 명제보다는 더 일반적인 판단을 이용하여 formal system에 적용가능하다. Curry-Howard isomophism을 항과 증명, 판단과 타입사이로 확장가능하다. 본 세미나에서는 Edinburgh대학에서 개발한 LEGO의 기본 계산법으로서 CC를 소개한다.

내용

  1. MIL (Minimal Implication Logic)
  2. Formal System
  3. Natural Deduction
  4. Normalization
  5. First-Order Logic
  6. Dependent Types
  7. Calculus of Constructions
  8. Polymorphisms in LEGO, MIL Formalized
  9. Weak Normalization
http://www.dcs.ed.ac.uk/home/als/Teaching/CAFR/

Resources

[ List ]