1 | @inproceedings{cil02, |
---|
2 | title = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs}, |
---|
3 | author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer}, |
---|
4 | booktitle = {Compiler Construction: 11th International Conference (CC 2002)}, |
---|
5 | pages = {213--228}, |
---|
6 | year = 2002, |
---|
7 | editor = {R. Nigel Horspool}, |
---|
8 | volume = 2304, |
---|
9 | series = {Lecture Notes in Computer Science}, |
---|
10 | publisher = {Springer}, |
---|
11 | doi = {10.1007/3-540-45937-5_16} |
---|
12 | } |
---|
13 | |
---|
14 | @article{compcert-mm08, |
---|
15 | title = {Formal Verification of a {C}-like Memory Model and Its Uses for Verifying Program Transformations}, |
---|
16 | author = {Xavier Leroy and Sandrine Blazy}, |
---|
17 | journal = {Journal of Automated Reasoning}, |
---|
18 | year = 2008, |
---|
19 | volume = 41, |
---|
20 | number = 1, |
---|
21 | pages = {1--31}, |
---|
22 | doi = {10.1007/s10817-008-9099-0} |
---|
23 | } |
---|
24 | |
---|
25 | Entry from ACM Digital Library. |
---|
26 | |
---|
27 | @inproceedings{1111042, |
---|
28 | author = {Xavier Leroy}, |
---|
29 | title = {Formal certification of a compiler back-end or: programming a compiler with a proof assistant}, |
---|
30 | booktitle = {POPL'06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, |
---|
31 | year = {2006}, |
---|
32 | isbn = {1-59593-027-2}, |
---|
33 | pages = {42--54}, |
---|
34 | location = {Charleston, South Carolina, USA}, |
---|
35 | doi = {http://doi.acm.org/10.1145/1111037.1111042}, |
---|
36 | publisher = {ACM Press}, |
---|
37 | address = {New York, NY, USA}, |
---|
38 | } |
---|
39 | |
---|
40 | @inproceedings{sozeau06, |
---|
41 | title = {Subset Coercions in {Coq}}, |
---|
42 | author = {Matthiue Sozeau}, |
---|
43 | booktitle = {Types for Proofs and Programs (TYPES 2006)}, |
---|
44 | year = 2007, |
---|
45 | editor = {Thorsten Altenkirch and Conor McBride}, |
---|
46 | volume = 4502, |
---|
47 | series = {Lecture Notes in Computer Science}, |
---|
48 | pages = {237--252}, |
---|
49 | publisher = {Springer-Verlag}, |
---|
50 | doi = {10.1007/978-3-540-74464-1_16} |
---|
51 | } |
---|
52 | |
---|
53 | @article{Moggi199155, |
---|
54 | title = "Notions of computation and monads", |
---|
55 | journal = "Information and Computation", |
---|
56 | volume = "93", |
---|
57 | number = "1", |
---|
58 | pages = "55 - 92", |
---|
59 | year = "1991", |
---|
60 | note = "Selections from 1989 IEEE Symposium on Logic in Computer Science", |
---|
61 | issn = "0890-5401", |
---|
62 | doi = "DOI: 10.1016/0890-5401(91)90052-4", |
---|
63 | url = "http://www.sciencedirect.com/science/article/B6WGK-4DX4K5F-P/2/a5ad300540b29452e7e41eed22de9e89", |
---|
64 | author = "Eugenio Moggi", |
---|
65 | abstract = " |
---|
66 | The [lambda]-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with [lambda]-terms. However, if one goes further and uses [beta][eta]-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results. In this paper we introduce calculi, based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation." |
---|
67 | } |
---|
68 | |
---|
69 | @misc{d2.1, |
---|
70 | title = {Compiler design and intermediate languages}, |
---|
71 | author = {Roberto M. Amadio and Nicolas Ayache and Yann R{\'{e}}gis-Gianas and Kayvan Memarian and Ronan Saillard}, |
---|
72 | howpublished = {Deliverable 2.1, Project FP7-ICT-2009-C-243881 CerCo}, |
---|
73 | } |
---|
74 | |
---|
75 | @book{schmidt86, |
---|
76 | title = "Denotational Semantics: A Methodology for Language Development", |
---|
77 | author = "David A. Schmidt", |
---|
78 | publisher = "Allyn and Bacon, Inc.", |
---|
79 | year = 1986 |
---|
80 | } |
---|