|
1
|
1 @article{
|
|
|
2 cbc,
|
|
|
3 author = "Kaito TOKKMORI and Shinji KONO",
|
|
|
4 title = "Implementing Continuation based language in LLVM and Clang",
|
|
|
5 journal = "LOLA 2015",
|
|
|
6 month = "July",
|
|
|
7 year = 2015
|
|
|
8 }
|
|
|
9
|
|
|
10 @article{moggi-monad,
|
|
|
11 author = {Moggi, Eugenio},
|
|
|
12 title = {Notions of Computation and Monads},
|
|
|
13 journal = {Inf. Comput.},
|
|
|
14 issue_date = {July 1991},
|
|
|
15 volume = {93},
|
|
|
16 number = {1},
|
|
|
17 month = jul,
|
|
|
18 year = {1991},
|
|
|
19 issn = {0890-5401},
|
|
|
20 pages = {55--92},
|
|
|
21 numpages = {38},
|
|
|
22 url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
|
|
|
23 doi = {10.1016/0890-5401(91)90052-4},
|
|
|
24 acmid = {116984},
|
|
|
25 publisher = {Academic Press, Inc.},
|
|
|
26 address = {Duluth, MN, USA},
|
|
|
27 }
|
|
|
28
|
|
|
29 @inproceedings{Yang:2010:SLI:1806596.1806610,
|
|
|
30 author = {Yang, Jean and Hawblitzel, Chris},
|
|
|
31 title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
|
|
|
32 booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
|
|
|
33 series = {PLDI '10},
|
|
|
34 year = {2010},
|
|
|
35 isbn = {978-1-4503-0019-3},
|
|
|
36 location = {Toronto, Ontario, Canada},
|
|
|
37 pages = {99--110},
|
|
|
38 numpages = {12},
|
|
|
39 url = {http://doi.acm.org/10.1145/1806596.1806610},
|
|
|
40 doi = {10.1145/1806596.1806610},
|
|
|
41 acmid = {1806610},
|
|
|
42 publisher = {ACM},
|
|
|
43 address = {New York, NY, USA},
|
|
|
44 keywords = {operating system, run-time system, type safety, verification},
|
|
|
45 }
|
|
|
46
|
|
|
47 @inproceedings{Klein:2009:SFV:1629575.1629596,
|
|
|
48 author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
|
|
|
49 title = {seL4: Formal Verification of an OS Kernel},
|
|
|
50 booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
|
|
|
51 series = {SOSP '09},
|
|
|
52 year = {2009},
|
|
|
53 isbn = {978-1-60558-752-3},
|
|
|
54 location = {Big Sky, Montana, USA},
|
|
|
55 pages = {207--220},
|
|
|
56 numpages = {14},
|
|
|
57 url = {http://doi.acm.org/10.1145/1629575.1629596},
|
|
|
58 doi = {10.1145/1629575.1629596},
|
|
|
59 acmid = {1629596},
|
|
|
60 publisher = {ACM},
|
|
|
61 address = {New York, NY, USA},
|
|
|
62 keywords = {isabelle/hol, l4, microkernel, sel4},
|
|
|
63 }
|
|
|
64
|
|
|
65 @inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
|
|
|
66 author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
|
|
|
67 title = {Push-button Verification of File Systems via Crash Refinement},
|
|
|
68 booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
|
|
|
69 series = {OSDI'16},
|
|
|
70 year = {2016},
|
|
|
71 isbn = {978-1-931971-33-1},
|
|
|
72 location = {Savannah, GA, USA},
|
|
|
73 pages = {1--16},
|
|
|
74 numpages = {16},
|
|
|
75 url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
|
|
|
76 acmid = {3026879},
|
|
|
77 publisher = {USENIX Association},
|
|
|
78 address = {Berkeley, CA, USA},
|
|
|
79 }
|
|
|
80
|
