source: Deliverables/D3.1/Report/report.bib @ 1833

Last change on this file since 1833 was 381, checked in by campbell, 9 years ago

Some d3.1 work.

File size: 3.2 KB
Line 
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
25Entry 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,
54title = "Notions of computation and monads",
55journal = "Information and Computation",
56volume = "93",
57number = "1",
58pages = "55 - 92",
59year = "1991",
60note = "Selections from 1989 IEEE Symposium on Logic in Computer Science",
61issn = "0890-5401",
62doi = "DOI: 10.1016/0890-5401(91)90052-4",
63url = "http://www.sciencedirect.com/science/article/B6WGK-4DX4K5F-P/2/a5ad300540b29452e7e41eed22de9e89",
64author = "Eugenio Moggi",
65abstract = "
66The [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,
70title = {Compiler design and intermediate languages},
71author = {Roberto M. Amadio and Nicolas Ayache and Yann R{\'{e}}gis-Gianas and Kayvan Memarian and Ronan Saillard},
72howpublished = {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}
Note: See TracBrowser for help on using the repository browser.