-
Notifications
You must be signed in to change notification settings - Fork 0
/
biblio.bib
109 lines (101 loc) · 3.3 KB
/
biblio.bib
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
@book{Lipovaca:2011:LYH:2018642,
author = {Lipovaca, Miran},
title = {Learn You a Haskell for Great Good!: A Beginner's Guide},
year = {2011},
isbn = {1593272839, 9781593272838},
edition = {1st},
publisher = {No Starch Press},
address = {San Francisco, CA, USA},
}
@ONLINE{SBV,
title = {SBV: SMT Based Verification in Haskell},
language = {english},
hyphenation = {english},
url = {http://leventerkok.github.io/sbv/},
urldate = {2017-11-27},
}
@ONLINE{IAMGithub,
title = {Inglorious Adding Machine},
language = {english},
hyphenation = {english},
url = {https://github.com/tuura/iam},
urldate = {2017-11-27},
}
@TECHREPORT{smtlib,
author = {Clark Barrett and Aaron Stump and Cesare Tinelli},
title = {{The SMT-LIB Standard: Version 2.0}},
institution = {Department of Computer Science, The University of Iowa},
year = 2010,
note = {Available at {\tt www.SMT-LIB.org}}
}
% F*
@inproceedings{Swamy:2016:DTM:2837614.2837655,
author = {Swamy, Nikhil and Hri\c{t}cu, C\u{a}t\u{a}lin and Keller, Chantal and Rastogi, Aseem and Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, C{\'e}dric and Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-B{\'e}guelin, Santiago},
title = {Dependent Types and Multi-monadic Effects in F*},
booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
series = {POPL '16},
year = {2016},
isbn = {978-1-4503-3549-2},
location = {St. Petersburg, FL, USA},
pages = {256--270},
numpages = {15},
url = {http://doi.acm.org/10.1145/2837614.2837655},
doi = {10.1145/2837614.2837655},
acmid = {2837655},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {effectful programming, proof assistants, verification},
}
% Idris
@article{JFP:9060502,
author = {BRADY,EDWIN},
title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
journal = {Journal of Functional Programming},
volume = {23},
issue = {05},
month = {9},
year = {2013},
issn = {1469-7653},
pages = {552--593},
numpages = {42},
doi = {10.1017/S095679681300018X},
URL = {http://journals.cambridge.org/article_S095679681300018X},
}
% Why3
@inproceedings{filliatre13esop,
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Why3 --- Where Programs Meet Provers},
booktitle = {Proceedings of the 22nd European Symposium on Programming},
month = mar,
year = 2013,
volume = {7792},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthias Felleisen and Philippa Gardner},
pages = {125--128},
hal = {http://hal.inria.fr/hal-00789533},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@article{Leveson2004,
author={Leveson, Nancy G.},
title={Role of Software in Spacecraft Accidents},
journal={Journal of Spacecraft and Rockets},
year={2004},
month={Jul},
day={01},
publisher={American Institute of Aeronautics and Astronautics},
volume={41},
number={4},
pages={564-575},
issn={0022-4650},
doi={10.2514/1.11950},
url={https://doi.org/10.2514/1.11950}
}