- Timestamp:
- Apr 24, 2019, 4:06:28 PM (5 years ago)
- Branches:
- ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum
- Children:
- 39de1c5
- Parents:
- 71a12390
- Location:
- doc
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
doc/bibliography/pl.bib
r71a12390 rec92b48 1148 1148 year = 1998, 1149 1149 note = {{\small\textsf{ftp://\-plg.uwaterloo.ca/\-pub/\-Cforall/\-refrat.ps.gz}}}, 1150 } 1151 1152 @phdthesis{Norrish98, 1153 title={C formalised in HOL}, 1154 author={Norrish, Michael}, 1155 year={1998}, 1156 school={University of Cambridge} 1150 1157 } 1151 1158 … … 3154 3161 year = 2018, 3155 3162 } 3163 3164 @article{Leroy09, 3165 keywords = {C formalization}, 3166 contributer = {a3moss@uwaterloo.ca}, 3167 author = {Leroy, Xavier}, 3168 title = {Formal Verification of a Realistic Compiler}, 3169 journal = {Commun. ACM}, 3170 issue_date = {July 2009}, 3171 volume = {52}, 3172 number = {7}, 3173 month = jul, 3174 year = {2009}, 3175 issn = {0001-0782}, 3176 pages = {107--115}, 3177 numpages = {9}, 3178 url = {http://doi.acm.org/10.1145/1538788.1538814}, 3179 doi = {10.1145/1538788.1538814}, 3180 acmid = {1538814}, 3181 publisher = {ACM}, 3182 address = {New York, NY, USA}, 3183 } 3156 3184 3157 3185 @manual{Fortran95, … … 5316 5344 } 5317 5345 5346 @inproceedings{Krebbers14, 5347 keywords = {c formalization}, 5348 contributer = {a3moss@uwaterloo.ca}, 5349 author = {Krebbers, Robbert}, 5350 title = {An Operational and Axiomatic Semantics for Non-determinism and Sequence Points in C}, 5351 booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 5352 series = {POPL '14}, 5353 year = {2014}, 5354 isbn = {978-1-4503-2544-8}, 5355 location = {San Diego, California, USA}, 5356 pages = {101--112}, 5357 numpages = {12}, 5358 url = {http://doi.acm.org/10.1145/2535838.2535878}, 5359 doi = {10.1145/2535838.2535878}, 5360 acmid = {2535878}, 5361 publisher = {ACM}, 5362 address = {New York, NY, USA}, 5363 } 5364 5318 5365 @book{Deitel04, 5319 5366 keywords = {concurrency, operating systems}, … … 7612 7659 } 7613 7660 7661 @techreport{Black90, 7662 title={Typechecking polymorphism in {Emerald}}, 7663 author={Black, Andrew P and Hutchinson, Norman C}, 7664 year={1990}, 7665 institution={Cambridge Research Laboratory, Digital Equipment Corporation} 7666 } 7667 7614 7668 @article{Cormack90, 7615 7669 keywords = {polymorphism}, -
doc/theses/aaron_moss_PhD/phd/background.tex
r71a12390 rec92b48 379 379 \CFA{} adds a significant number of features to standard C, increasing the expressivity and re-usability of \CFA{} code while maintaining backwards compatibility for both code and larger language paradigms. 380 380 This flexibility does incur significant added compilation costs, however, the mitigation of which are the primary concern of this thesis. 381 382 \cbstarty 383 One area of inquiry which is outside the scope of this thesis is formalization of the \CFA{} type system. 384 Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus which is the theoretical basis for the \CFA{} type system. 385 Ditchfield did not, however, prove any soundness or completeness properties for $F_\omega^\ni$; such proofs remain future work. 386 A number of formalisms other than $F_\omega^\ni$ could potentially be adapted to model \CFA{}. 387 One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types which are conceptually similar to \CFA{} traits. 388 These modelling approaches could potentially be used to extend an existing formal semantics for C such as Cholera \cite{Norrish98}, CompCert \cite{Leroy09}, or Formalin \cite{Krebbers14}. 389 \cbendy -
doc/theses/aaron_moss_PhD/phd/thesis.tex
r71a12390 rec92b48 36 36 \newcommand{\cbstartx}{\cbcolor{red} \cbstart} 37 37 \newcommand{\cbendx}{\cbend \cbcolor{blue}} 38 \newcommand{\cbstarty}{\cbcolor{green} \cbstart} 39 \newcommand{\cbendy}{\cbend \cbcolor{blue}} 38 40 39 41 % Hyperlinks make it very easy to navigate an electronic document.
Note: See TracChangeset
for help on using the changeset viewer.