Changeset ec92b48


Ignore:
Timestamp:
Apr 24, 2019, 4:06:28 PM (5 years ago)
Author:
Aaron Moss <a3moss@…>
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
Message:

thesis: add comments on CFA formalization

Location:
doc
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • doc/bibliography/pl.bib

    r71a12390 rec92b48  
    11481148    year        = 1998,
    11491149    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}
    11501157}
    11511158
     
    31543161    year        = 2018,
    31553162}
     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}
    31563184
    31573185@manual{Fortran95,
     
    53165344}
    53175345
     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
    53185365@book{Deitel04,
    53195366    keywords    = {concurrency, operating systems},
     
    76127659}
    76137660
     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
    76147668@article{Cormack90,
    76157669    keywords    = {polymorphism},
  • doc/theses/aaron_moss_PhD/phd/background.tex

    r71a12390 rec92b48  
    379379\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.
    380380This flexibility does incur significant added compilation costs, however, the mitigation of which are the primary concern of this thesis.
     381
     382\cbstarty
     383One area of inquiry which is outside the scope of this thesis is formalization of the \CFA{} type system.
     384Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus which is the theoretical basis for the \CFA{} type system.
     385Ditchfield did not, however, prove any soundness or completeness properties for $F_\omega^\ni$; such proofs remain future work.
     386A number of formalisms other than $F_\omega^\ni$ could potentially be adapted to model \CFA{}.
     387One 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.
     388These 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  
    3636\newcommand{\cbstartx}{\cbcolor{red} \cbstart}
    3737\newcommand{\cbendx}{\cbend \cbcolor{blue}}
     38\newcommand{\cbstarty}{\cbcolor{green} \cbstart}
     39\newcommand{\cbendy}{\cbend \cbcolor{blue}}
    3840
    3941% Hyperlinks make it very easy to navigate an electronic document.
Note: See TracChangeset for help on using the changeset viewer.