-
Notifications
You must be signed in to change notification settings - Fork 0
/
Postscript.v
106 lines (83 loc) · 3.55 KB
/
Postscript.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
(** * Postscript *)
(** * Looking back... *)
(** - _Functional programming_
- "declarative" programming (recursion over persistent data
structures)
- higher-order functions
- polymorphism *)
(**
- _Logic_, the mathematical basis for software engineering:
<<
logic calculus
-------------------- = ----------------------------
software engineering mechanical/civil engineering
>>
- inductively defined sets and relations
- inductive proofs
- proof objects *)
(**
- _Coq_, an industrial-strength proof assistant
- functional core language
- core tactics
- automation
*)
(**
- _Foundations of programming languages_
- notations and definitional techniques for precisely specifying
- abstract syntax
- operational semantics
- big-step style
- small-step style
- type systems
- program equivalence
- Hoare logic
- fundamental metatheory of type systems
- progress and preservation
- theory of subtyping
*)
(* ###################################################################### *)
(** * Looking forward... *)
(** Some good places to go for more...
- Several optional chapters of _Software Foundations_
- Cutting-edge conferences on programming languages and formal
verification:
- POPL
- PLDI
- OOPSLA
- ICFP
- CAV
- (and many others)
- More on functional programming
- Learn You a Haskell for Great Good, by Miran
Lipovaca (ebook)
- and many other texts on Haskell, OCaml, Scheme, Scala, ...
- More on Hoare logic and program verification
- The Formal Semantics of Programming Languages: An
Introduction, by Glynn Winskel. MIT Press, 1993.
- Many practical verification tools, e.g. Microsoft's
Boogie system, Java Extended Static Checking, etc.
- More on the foundations of programming languages:
- Types and Programming Languages, by Benjamin C. Pierce. MIT
Press, 2002.
- Practical Foundations for Programming Languages, by Robert
Harper. Forthcoming from MIT Press. Manuscript available
from his web page.
- Foundations for Programming Languages, by John C. Mitchell.
MIT Press, 1996.
- More on Coq:
- Certified Programming with Dependent Types, by Adam
Chlipala. A draft textbook on practical proof
engineering with Coq, available from his web page.
- Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions, by Yves
Bertot and Pierre Casteran. Springer-Verlag, 2004.
- Iron Lambda (http://iron.ouroborus.net/) is a collection
of Coq formalisations for functional languages of
increasing complexity. It fills part of the gap between
the end of the Software Foundations course and what
appears in current research papers. The collection has
at least Progress and Preservation theorems for a number
of variants of STLC and the polymorphic
lambda-calculus (System F)
*)
(* $Date: 2014-08-23 15:24:59 -0400 (Sat, 23 Aug 2014) $ *)