Languages

Summer School

暑期实践课程 

 

2 Emacs

  • 下载Emacs,解压到任意路径.
  • 下载".emacs"
  • 设置环境变量HOME为".emacs"文件所在目录.
  • 下载"tuareg-mode"和"proofgeneral",并解压缩到Emacs/site-lisp
  • 根据解压的路径修改".emacs"

3 OCaml 与 Coq

下载Ocaml, Coq后, 运行安装程序即可

4 OCaml资料

5 Coq资料

6 ESC/Java安装 

  • 下载 ESC/Java 的集成环境
  • 下载并安装JDK 1.4和JDK 1.6
  • 按照PPT配置Eclipse和ESC/Java,重点在于指定创建工程使用的java编译器版本
  • ESC/Java的相关资料: 介绍ESC/Java的文章, 官方文档
  • 推荐调研和使用Spec#
 

 

AttachmentSize
Lecture1.ppt667 KB
ProofGeneral.rar2.29 MB
dotemacs.rar206 bytes
tuareg.rar26.24 KB
Lab1.rar23.58 KB
Intro.ppt482 KB
Lec1-Overview.pdf485.47 KB
Lec2-CurryHoward.pdf374.34 KB
coq.ppt842 KB
logic_prac.rar4.44 KB
logic_solution.rar4.69 KB
certifyingcompiler.ppt856.5 KB
lab3_final.zip25.47 KB
lab3_solution.zip1.84 KB
Lecture4.zip3.88 MB
lab4.zip31.8 KB
concurrency.pdf1.42 MB
lab5.zip5.75 KB
ESC.ppt305.5 KB
Lec5-6.pdf3.22 MB