4541.574 Programming Language Theory

À̱¤±Ù Kwangkeun Yi
Programming Research Lab./CSE/Seoul National University

°­ÀÇ: ¿ù/¼ö 16:00-17:15 @ 302µ¿ 317-2È£

¸ñÇ¥ Objectives

ÀÌ °­ÀÇÀÇ ¸ñÇ¥´Â ÇÁ·Î±×·¡¹Ö ¾ð¾î ºÐ¾ß¿¡¼­ ÃàÀûµÈ ÁÖ¿ä ³»¿ë°ú ±×°ÍÀ» ¾ö¹ÐÇÏ°Ô Ç¥ÇöÇÏ°í ÀÀ¿ëÇÏ´Â °úÇÐÀûÀÎ ¼Ø¾¾¸¦ ÀÍÈ÷°Ô ÇÏ´Â °ÍÀÌ´Ù.

ÀÌ·¯ÇÑ °­ÀÇ°¡ ¿Ö ÇÊ¿äÇÑ °ÍÀϱî?

  • ¼ÒÇÁÆ®¿þ¾î ÀÌ·ÐÀÇ ¸¹Àº ±âÃÊ°¡ ÇÁ·Î±×·¡¹Ö ¾ð¾î ÀÌ·ÐÀ» ÇнÀÇϸ鼭 È¿°úÀûÀ¸·Î ÁغñµÈ´Ù.
  • ¼ÒÇÁÆ®¿þ¾î¿¡ ´ëÇÑ "¾ö¹ÐÇÑ"(formal) ³í¹®À» ÀÐ°í ¾²´Â µ¥ Àͼ÷ÇØ Áø´Ù. ¼ÒÇÁÆ®¿þ¾î¸¦ ¸ðµ¨ÇÏ°í ±â¼úÇÏ°í »ìÆ캸°í È®ÀÎÇÏ¸ç ±× ¼ºÁúÀÇ ÁÁÀº Á¡À» ¼³µæÇÏ´Â ³í¹®À» ¾²´Â ¹æ½ÄÀ» ÀÍÈ÷°Ô µÈ´Ù.
  • °íºÎ°¡ ¼ÒÇÁÆ®¿þ¾î °³¹ßÀº ³ª³¯È÷ ¾ö¹ÐÇÑ ±â¼úÀÌ µÇ°¡°í ÀÖ°í, ±× ÇÑ ÃàÀÌ º¸´Ù Á¤±³ÇÏ°í Æí¸®ÇÑ Å¸ÀÔ ½Ã½ºÅÛÀ» °®Ãá ÇÁ·Î±×·¡¹Ö ¾ð¾îÀÇ »ç¿ëÀÌ´Ù.
  • ´ëºÎºÐÀÇ ¼ÒÇÁÆ®¿þ¾î ½Ã½ºÅÛµéÀÌ ÄÄÇ»ÅÍ ¾ð¾î¸¦ ó¸®ÇÏ´Â ºÎÇ°À» Ç°°í ÀÖ°Ô µÇ´Âµ¥, ÀÌ ºÎÇ°µéÀÌ ÇÁ·Î±×·¡¹Ö ¾ð¾î ºÐ¾ß¿¡¼­ ÃàÀûÇÑ À̷аú ½ÇÁ¦¿¡ ´ëÇÑ ¼º°ú¸¦ ÀÌÇØÇÏ°í ¼³°èµÉ ÇÊ¿ä°¡ ÀÖ´Ù.

³»¿ë Contents

  • °¡·Î
    • Semantic formalisms: natural semantics, structural operational semantics, abstract machine semantics, evaluation contexts
    • Proof techniques/principles: induction, structural induction, fixpoint induction, induction on proof size, logical relation
  • ¼¼·Î
    • Preliminaries: abstract syntax, binding, scope, renaming, compositional semantics, logics and inference
    • Lambda Calculus: operational semantics, normal-order/eager-order reduction, Church thesis, lambda encodings, domain theory
    • Applicative Language: datatypes, functions, exceptions, continuations, continuation-passing-style transformation, abstract machines
    • Type System: monomorphic type system, polymorphic type system, existential type system, subtype system, typeful compilation

±ÔÁ¤ Policy

  mid term: 50%, final: 50%
  • ¼ºÀûÀº Àý´ëÆò°¡.
  • Ãâ¼® 100%´Â Çʼö. ¾î¿ ¼ö ¾ø´Â °æ¿ì´Â ¹Ýµå½Ã »çÀü Çã¶ôÀ» ¹Þ´Â´Ù.

¼÷Á¦ Homeworks

 

Áøµµ¹× ÀÚ·á Slides & Resources

wk 1 part -1: induction, logic, inference, proofs slide0, book5-24, slide1                    
wk 2 part -1: abstract syntax, operational semantics slide2  
wk 3 part 0: HOT (higher-order & typed) programming I slide3
wk 4 part 0: HOT programming II slide4
wk 5 language model: lambda calculus slide5, slide6, slide7
wk 6 simply typed lambda calculus slide8, slide9, slide10
wk 7 extensions on to a real language slide11, slide12, slide13
wk 8 simple type reconstruction slide14
wk 9 let-polymorhpic types slide15
wk 10 let-polymorphic type reconstruction slide16
wk 11 subtypes slide17, slide18 New!, slide19 New!
wk 12 existential types, recursive types
  • ±³Àç/Textbooks

    ÀÐÀ» ³í¹® Papers

  • © Copyright 2007, ÀÌ ±¤±Ù Kwangkeun Yi