Programming in Martin-Lof's Type Theory
Programming in Martin-Löf's Type Theory An Introduction Bengt Nordström Kent Petersson Jan M. Smith Department of Computing Sciences University of Göteborg / Chalmers S-412 96 Göteborg Sweden This book was published by Oxford University Press in 1990. It is now out of print. This version is available from www.cs.chalmers.se/Cs/Research/Logic/book. Table of contents in Postscript. The whole book (2
Programs and Proofs
Mechanizing Mathematics with Dependent Types Lecture notes with exercises Ilya Sergey These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reason
ATSプログラミング入門
この本は Introduction to Programming in ATS の日本語訳です。 日本語訳の維持管理は JATS-UG - Japan ATS User Group が行なっています。 翻訳に参加するには ATS2公式マニュアルの日本語訳 を参照してください。 プログラミング言語としての ATS は豊かな構文と機能を両立しています。 この本では ATS の中心となる機能を読者に解説します。 それらは基本的な関数型プログラミング、単純な型、(再帰的に定義された) データ型、多相型、依存型、線形型、定理証明、定理証明によるプログラミング (PwTP)、そしてテンプレートを使ったプログラミングなどです。 一般的なプログラミングに馴染みのある読者を仮定してませんが、この本は相当のプログラミング経験のない読者には少し難しいかもしれません。 All rights are reserve
MagicHaskeller: An Inductive Functional Programming System for Casual/Beginner Haskell Programmers
MagicHaskeller: An Inductive Functional Programming System for Casual/Beginner Haskell Programmers Susumu Katayama, University of Miyazaki 日本語(Japanese) Spanish page by ChicksX.com Thanks for the translation! (The award-winning reinforcement learner using MagicHaskeller is at the end of this page.) (There is also an experimental variant of MagicHaskeller which synthesizes functions for Microsoft E
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
FGJ-omega's home page
http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/book1.html
The Delphin Project
PLPV 2013
Yale FLINT Group: A Syntactic Approach to FPCC