"Partial recursive functions in Martin-Lof type theory" (Anton Setzer)

15時10分より16時40分まで。partial recursive functionをMartin-Lof type theoryで表現する。inductive definitionをtypeで表現するとき、普通にやるとstrictlyにpositiveなindexed definition でなくなるものが出てくるので、”indexed inductive recursive definition"に拡張する。最後はnormal form theoremまで到達。
はい、とてもtechnicalなお話でした。想定聴衆はcomputer scienceの人か。