{"author_name":"umedaikiti","height":"190","author_url":"https://blog.hatena.ne.jp/umedaikiti/","categories":[],"url":"https://umedaikiti.hatenablog.com/entry/2015/12/13/194344","width":"100%","provider_name":"Hatena Blog","version":"1.0","html":"<iframe src=\"https://hatenablog-parts.com/embed?url=https%3A%2F%2Fumedaikiti.hatenablog.com%2Fentry%2F2015%2F12%2F13%2F194344\" title=\"pCIC\u306b\u3064\u3044\u3066 - Sis puella magica!\" class=\"embed-card embed-blogcard\" scrolling=\"no\" frameborder=\"0\" style=\"display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;\"></iframe>","title":"pCIC\u306b\u3064\u3044\u3066","image_url":"http://chart.apis.google.com/chart?cht=tx&chl=%20%28S%2C%20A%2C%20R%29","blog_title":"Sis puella magica!","blog_url":"https://umedaikiti.hatenablog.com/","description":"TSG Advent Calendar 2015 - Adventar\u306e12/13\u306e\u8a18\u4e8b\u3067\u3059\u3002 \u5e8f\u6587 - pCIC\u3068\u306f pCIC\u306fPredicative Calculus of (Co)Inductive Constructions\u306e\u3053\u3068\u3067\u3001coq\u306e\u578b\u30b7\u30b9\u30c6\u30e0\u306e\u3053\u3068\u3067\u3059\u3002 \u5b9a\u7406\u8a3c\u660e\u652f\u63f4\u7cfb\u3068\u8a00\u308f\u308c\u308bcoq\u3067\u3059\u304c\u3001\u305d\u3082\u305d\u3082coq\u3067\u300c\u8a3c\u660e\u3059\u308b\u300d\u3068\u306f\u3069\u3046\u3044\u3046\u3053\u3068\u3067\u3057\u3087\u3046\u304b\u3002 coq\u306b\u304a\u3051\u308b\u547d\u984c\u306f\u578b(type)\u306b\u3001\u305d\u306e\u8a3c\u660e\u306f\u9805(term)\u306b\u5bfe\u5fdc\u3057\u3066\u3044\u307e\u3059(Curry-Howard\u540c\u578b\u3092\u601d\u3044\u51fa\u3057\u3066\u304f\u3060\u3055\u3044)\u3002\u3064\u307e\u308a\u3001coq\u3067\u3042\u308b\u547d\u984cP\u3092\u8a3c\u660e\u3059\u308b\u3068\u3044\u3046\u3053\u3068\u306f\u3001\u578bP\u3092\u6301\u3064\u9805\u3092\u63a2\u3057\u3066\u304f\u308b\u3053\u3068\u306b\u5bfe\u5fdc\u3057\u3066\u3044\u307e\u3059\u3002 \u2026","type":"rich","published":"2015-12-13 19:43:44","provider_url":"https://hatena.blog"}