Changeset 39de1c5 for doc/theses/aaron_moss_PhD/phd/introduction.tex
- Timestamp:
- Apr 24, 2019, 4:09:47 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:
- 5d3a952
- Parents:
- ec92b48
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
doc/theses/aaron_moss_PhD/phd/introduction.tex
rec92b48 r39de1c5 51 51 \cbendx 52 52 Type environments are also widely modelled in compiler implementations, particularly for functional languages, though also increasingly commonly for other languages (such as Rust~\cite{Rust}) which perform type inference; the type environment presented here may be useful to those language implementors. 53 54 \cbstarty 55 One area of inquiry which is outside the scope of this thesis is formalization of the \CFA{} type system. 56 Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus which is the theoretical basis for the \CFA{} type system. 57 Ditchfield did not, however, prove any soundness or completeness properties for $F_\omega^\ni$; such proofs remain future work. 58 A number of formalisms other than $F_\omega^\ni$ could potentially be adapted to model \CFA{}. 59 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. 60 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}. 61 \cbendy
Note: See TracChangeset
for help on using the changeset viewer.