From faca758c348718411803e4b8fab3a83a85665d1a Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Wed, 24 May 2017 15:28:12 +0200 Subject: [PATCH] update stukje over ivory --- acronyms.tex | 1 - glossaries.tex | 3 --- introduction.tex | 13 +++++++++---- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/acronyms.tex b/acronyms.tex index 2481539..ac1d001 100644 --- a/acronyms.tex +++ b/acronyms.tex @@ -12,5 +12,4 @@ \newacronym{TCP}{TCP}{Transmission Control Protocol} \newacronym{RFID}{RFID}{Radio-Frequency Identification} \newacronym{GPS}{GPS}{Global Positioning System} -\newacronym{RTOS}{RTOS}{Real-Time Operating System} \newacronym{LCD}{LCD}{Liquid Crystal Display} diff --git a/glossaries.tex b/glossaries.tex index d05ca70..8b19444 100644 --- a/glossaries.tex +++ b/glossaries.tex @@ -12,9 +12,6 @@ \newglossaryentry{Ivory}{name=Ivory, description={is a type-safe \gls{EDSL} designed to generate \gls{C}-code for high-assurance low-level systems}} -\newglossaryentry{Tower}{name=Tower, - description={is a type-safe \gls{EDSL} similar to \gls{Ivory} designed to - generate code for \acrlong{RTOS}}} \newglossaryentry{Task}{name=Task, description={is the basic building block of a \acrshort{TOP} system}} \newglossaryentry{mTask}{name=mTask, diff --git a/introduction.tex b/introduction.tex index 654cb1f..36ef589 100644 --- a/introduction.tex +++ b/introduction.tex @@ -114,8 +114,13 @@ Again, this requires a reprogramming cycle every time the Another \gls{EDSL} designed to generate low-level high-assurance programs is called \gls{Ivory} and uses \gls{Haskell} as a host language% \cite{elliott_guilt_2015}. The language uses the \gls{Haskell} type-system to -make unsafe language type safe. \gls{Ivory} has been used in for example the +make unsafe languages type safe. \gls{Ivory} has been used in for example the automotive industry to program parts of an autopilot% -\cite{pike_programming_2014}\cite{hickey_building_2014}. A dialect of the -\gls{Ivory} called \gls{Tower} has also been created by the same authors which -is has specific backends for \glspl{RTOS}. +\cite{pike_programming_2014}\cite{hickey_building_2014}. \Gls{Ivory}'s syntax +is deeply embedded but the type system is shallowly embedded. This requires +several \gls{Haskell} extensions that offer dependant type constructions. The +process of compiling an \gls{Ivory} program happens in stages. The embedded +code is transformed into an \gls{AST} that is sent to a backend. The +\gls{mTask} \gls{EDSL} transform the embedded code during compile-time directly +into the backend which is often a state transformer that will execute on +runtime.\todo{Misschien een beetje onduidelijk of kort?} -- 2.20.1