Add a few more bookmarks.
Chris Pressey
1 year, 1 month ago
23 | 23 |
* author: Adam Chlipala
|
24 | 24 |
* date: 2013
|
25 | 25 |
* online @ [archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes)
|
|
26 |
* booksite: http://adam.chlipala.net/cpdt/
|
26 | 27 |
* rating: TODO
|
27 | 28 |
|
28 | 29 |
I haven't read it, but this is an open-access book about Coq.
|
35 | 35 |
### Papers
|
36 | 36 |
|
37 | 37 |
[Hygiene-Compatible Macros in an Unhygienic Macro System.pdf](https://guenchi.github.io/Scheme/doc/Hygiene-Compatible%20Macros%20in%20an%20Unhygienic%20Macro%20System.pdf)
|
|
38 |
|
|
39 |
[Binding as Sets of Scopes](https://www.cs.utah.edu/plt/scope-sets/)
|
12 | 12 |
* rating: TODO
|
13 | 13 |
|
14 | 14 |
.
|
|
15 |
|
|
16 |
### Binding as Sets of Scopes
|
|
17 |
|
|
18 |
* url: https://www.cs.utah.edu/plt/scope-sets/
|
|
19 |
* rating: TODO
|
|
20 |
|
|
21 |
.
|
22 | 22 |
|
23 | 23 |
[CSE 40431/60431: Programming Languages (2022 course notes)](https://www3.nd.edu/~dchiang/teaching/pl/2022/)
|
24 | 24 |
|
|
25 |
[language design - Why F\#, Rust and Others Use Option Type Instead Of Nullable types like C\# 8 Or TypeScript? - Software Engineering Stack Exchange](https://softwareengineering.stackexchange.com/questions/410724/why-f-rust-and-others-use-option-type-instead-of-nullable-types-like-c-8-or-t)
|
|
26 |
|
|
27 |
[language design - Why do \"checked exceptions\", i.e., \"value-or-error return values\", work well in Rust and Go but not in Java? - Software Engineering Stack Exchange](https://softwareengineering.stackexchange.com/questions/420898/why-do-checked-exceptions-i-e-value-or-error-return-values-work-well-in)
|
|
28 |
|
25 | 29 |
### Compilation
|
26 | 30 |
|
27 | 31 |
[compiling - Do C compilers discard unused functions when statically linking to .a file? - Unix & Linux Stack Exchange](https://unix.stackexchange.com/questions/715899/do-c-compilers-discard-unused-functions-when-statically-linking-to-a-file)
|
48 | 48 |
|
49 | 49 |
.
|
50 | 50 |
|
|
51 |
### language design - Why F\#, Rust and Others Use Option Type Instead Of Nullable types like C\# 8 Or TypeScript? - Software Engineering Stack Exchange
|
|
52 |
|
|
53 |
* url: https://softwareengineering.stackexchange.com/questions/410724/why-f-rust-and-others-use-option-type-instead-of-nullable-types-like-c-8-or-t
|
|
54 |
* rating: TODO
|
|
55 |
|
|
56 |
.
|
|
57 |
|
|
58 |
### language design - Why do \"checked exceptions\", i.e., \"value-or-error return values\", work well in Rust and Go but not in Java? - Software Engineering Stack Exchange
|
|
59 |
|
|
60 |
* url: https://softwareengineering.stackexchange.com/questions/420898/why-do-checked-exceptions-i-e-value-or-error-return-values-work-well-in
|
|
61 |
* rating: TODO
|
|
62 |
|
|
63 |
.
|
|
64 |
|
51 | 65 |
### Compilation
|
52 | 66 |
|
53 | 67 |
* is-heading: true
|
17 | 17 |
* https://gutenberg.org/ebooks/974 (The Secret Agent: A Simple Tale by Joseph Conrad \| Project Gutenberg)
|
18 | 18 |
* https://gutenberg.org/ebooks/2775 (The Good Soldier by Ford Madox Ford \| Project Gutenberg)
|
19 | 19 |
|
|
20 |
### PLDI
|
|
21 |
|
|
22 |
* https://softwareengineering.stackexchange.com/questions/410724/why-f-rust-and-others-use-option-type-instead-of-nullable-types-like-c-8-or-t (language design - Why F\#, Rust and Others Use Option Type Instead Of Nullable types like C\# 8 Or TypeScript? - Software Engineering Stack Exchange)
|
|
23 |
* https://softwareengineering.stackexchange.com/questions/420898/why-do-checked-exceptions-i-e-value-or-error-return-values-work-well-in (language design - Why do \"checked exceptions\", i.e., \"value-or-error return values\", work well in Rust and Go but not in Java? - Software Engineering Stack Exchange)
|
|
24 |
|
20 | 25 |
### Philosophy
|
21 | 26 |
|
22 | 27 |
* https://htmlgiant.com/random/the-beginners-guide-to-hegel/ (HTMLGIANT / The Beginner's Guide to Hegel)
|
23 | 28 |
* https://plato.stanford.edu/entries/computer-science/ (The Philosophy of Computer Science (Stanford Encyclopedia of Philosophy))
|
|
29 |
|
|
30 |
### Type Systems
|
|
31 |
|
|
32 |
* https://www.pl.cs.jhu.edu/projects/type-constraints/ (Type Constraints · The Programming Languages Laboratory)
|
|
33 |
* https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types (The algebra (and calculus!) of algebraic data types)
|
|
34 |
* https://stackoverflow.com/questions/196465/what-is-a-type-and-effect-system (What is a type and effect system? - Stack Overflow)
|
24 | 35 |
|
25 | 36 |
TODO rated Books
|
26 | 37 |
--------------
|
|
130 | 141 |
### Macros
|
131 | 142 |
|
132 | 143 |
* https://guenchi.github.io/Scheme/doc/Hygiene-Compatible%20Macros%20in%20an%20Unhygienic%20Macro%20System.pdf (Hygiene-Compatible Macros in an Unhygienic Macro System.pdf)
|
|
144 |
* https://www.cs.utah.edu/plt/scope-sets/ (Binding as Sets of Scopes)
|
133 | 145 |
|
134 | 146 |
### Model Checking
|
135 | 147 |
|
16 | 16 |
|
17 | 17 |
[Coeffects: The next big programming challenge - Tomas Petricek](http://tomasp.net/blog/2014/why-coeffects-matter/)
|
18 | 18 |
|
|
19 |
[Type Constraints · The Programming Languages Laboratory](https://www.pl.cs.jhu.edu/projects/type-constraints/)
|
|
20 |
|
|
21 |
[The algebra (and calculus!) of algebraic data types](https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types)
|
|
22 |
|
|
23 |
[What is a type and effect system? - Stack Overflow](https://stackoverflow.com/questions/196465/what-is-a-type-and-effect-system)
|
|
24 |
|
19 | 25 |
### Papers
|
20 | 26 |
|
21 | 27 |
Should Your Specification Language Be Typed? (online @ [lamport.azurewebsites.net](http://lamport.azurewebsites.net/pubs/lamport-types.pdf) (PDF))
|
26 | 26 |
* rating: 1
|
27 | 27 |
|
28 | 28 |
.
|
|
29 |
|
|
30 |
### Type Constraints · The Programming Languages Laboratory
|
|
31 |
|
|
32 |
* url: https://www.pl.cs.jhu.edu/projects/type-constraints/
|
|
33 |
* rating: TODO
|
|
34 |
|
|
35 |
.
|
|
36 |
|
|
37 |
### The algebra (and calculus!) of algebraic data types
|
|
38 |
|
|
39 |
* url: https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types
|
|
40 |
* rating: TODO
|
|
41 |
|
|
42 |
.
|
|
43 |
|
|
44 |
### What is a type and effect system? - Stack Overflow
|
|
45 |
|
|
46 |
* url: https://stackoverflow.com/questions/196465/what-is-a-type-and-effect-system
|
|
47 |
* rating: TODO
|
|
48 |
|
|
49 |
.
|