-
Notifications
You must be signed in to change notification settings - Fork 0
/
Postscript.v
112 lines (86 loc) · 3.85 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
106
107
108
109
110
111
112
(** * Postscript *)
(** Congratulations: You've made it to the end! *)
(* ################################################################# *)
(** * Looking Back... *)
(** We've covered a lot of ground. The topics might be summarized like this:
- _Functional programming_:
- "declarative" programming style (recursion over persistent
data structures, rather than looping over mutable arrays
or pointer 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...
- This book includes several optional chapters covering topics
that you may find useful. If you've been using it in the
context of a course, take a look at the table of contents
and the chapter dependency diagram.
- 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 [Lipovaca 2011].
- 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 [Winskel 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 [Pierce 2002].
- Practical Foundations for Programming Languages, by
Robert Harper [Harper 2016].
- Foundations for Programming Languages, by John
C. Mitchell [Mitchell 1996].
- More on Coq:
- Certified Programming with Dependent Types, by Adam
Chlipala [Chlipala 2013].
- Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions, by Yves
Bertot and Pierre Casteran [Bertot 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: 2016-05-26 17:51:14 -0400 (Thu, 26 May 2016) $ *)