Changeset ec92b48 for doc/theses


Ignore:
Timestamp:
Apr 24, 2019, 4:06:28 PM (3 years ago)
Author:
Aaron Moss <a3moss@…>
Branches:
aaron-thesis, arm-eh, cleanup-dtors, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr
Children:
39de1c5
Parents:
71a12390
Message:

thesis: add comments on CFA formalization

Location:
doc/theses/aaron_moss_PhD/phd
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • 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.