Add polyglossia for supporting Greek/English

We have an issue with fonts, try to figure out how to make this
parametric.  We also have an issue with appendix numbers in Greek
(that's why I have "numerals=arabic" for greek).

Styles/softlab-thesis.cls

@@ -262,28 +262,52 @@
 % Required packages
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \RequirePackage{graphicx}
-\RequirePackage[english]{babel}
 \RequirePackage{fontspec}
 \RequirePackage{xunicode}
 \RequirePackage{xltxtra}
 \defaultfontfeatures{Mapping=tex-text}
-\RequirePackage{xgreek}
 
 % XeLaTeX fonts
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % roman font
-\setmainfont{Times New Roman}
+\def\font@roman{Times New Roman}
+%\def\font@roman{Liberation Serif}
 
 % sans serif font
-\setsansfont[Scale=MatchLowercase]{Arial}
+\def\font@sans{Arial}
+%\def\font@sans{Liberation Sans}
 
 % typewriter font
-\setmonofont[Scale=MatchLowercase]{Liberation Mono}
-%\setmonofont[Scale=MatchLowercase]{DejaVu Sans Mono}
-%\setmonofont[Scale=MatchLowercase]{Lucida Sans Typewriter}
-%\setmonofont[Scale=MatchLowercase]{Free Monospaced}
-%\setmonofont[Scale=MatchLowercase]{Bitstream Vera Sans Mono}
+\def\font@tt{Liberation Mono}
+%\def\font@tt{DejaVu Sans Mono}
+%\def\font@tt{Lucida Sans Typewriter}
+%\def\font@tt{Free Monospaced}
+%\def\font@tt{Bitstream Vera Sans Mono}
+
+\setromanfont{\font@roman}
+\setsansfont[Scale=MatchLowercase]{\font@sans}
+\setmonofont[Scale=MatchLowercase]{\font@tt}
+
+
+% Polyglossia
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\RequirePackage{polyglossia}
+\if@greek
+\newfontfamily\greekfont{\font@roman}
+\newfontfamily\greekfontsf[Scale=MatchLowercase]{\font@sans}
+\newfontfamily\greekfonttt[Script=grek,Scale=MatchLowercase]{\font@tt}
+%\newfontfamily\greekfont{Times New Roman}
+%\newfontfamily\greekfont[Script=grek]{Liberation Serif}
+%\newfontfamily\greekfontsf[Scale=MatchLowercase]{Arial}
+%\newfontfamily\greekfontsf[Script=grek,Scale=MatchLowercase]{Liberation Sans}
+%\newfontfamily\greekfonttt[Script=grek,Scale=MatchLowercase]{Liberation Mono}
+\setdefaultlanguage[variant=mono,numerals=arabic]{greek}
+\setotherlanguage{english}
+\else
+\setdefaultlanguage{english}
+\fi
 
 % Headings
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -719,17 +743,23 @@
   \let\maketitle\relax%
 }
 \def\abstractgr{%
-  \setlanguage{monogreek}%
+  \begin{greek}%
   \chapter*{\abstractnamegr\@mkboth{\abstractnamegr}{\abstractnamegr}}%
   \addcontentsline{toc}{chapter}{\abstractnamegr}%
   \noindent\ignorespaces}
-\def\endabstractgr{\par\vfil\null}
+\def\endabstractgr{%
+  \par%
+  \end{greek}%
+  \vfil\null}
 \def\abstracten{%
-  \selectlanguage{english}%
+  \begin{english}%
   \chapter*{\abstractnameen\@mkboth{\abstractnameen}{\abstractnameen}}%
   \addcontentsline{toc}{chapter}{\abstractnameen}%
   \noindent\ignorespaces}
-\def\endabstracten{\par\vfil\null}
+\def\endabstracten{%
+  \par%
+  \end{english}%
+  \vfil\null}
 
 % Sectioning
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -810,7 +840,11 @@
          \fi
       \fi%
       \refstepcounter{chapter}%
+      \if@mainmatter%
         \typeout{\chaptername\space\thechapter.}
+      \else%
+        \typeout{\appendixname\space\thechapter.}
+      \fi%
       \addcontentsline{toc}{chapter}{%
          \protect\numberline{\thechapter.}#1}%
    \else
@@ -907,9 +941,9 @@
     \part*{\appendixname\@mkboth{\appendixname}{\appendixname}%%
            \@addappendixtocontents}
   \else%
-    \renewcommand{\@chapapp}{\appendixname}%
+    \gdef\@chapapp{\appendixname}%
   \fi
-  \renewcommand{\thechapter}{\Alph{chapter}}}
+  \gdef\thechapter{\@Alph\c@chapter}}
 
 % Space lengths
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1411,8 +1445,10 @@
 
 % More environments
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\newenvironment{keywordsgr}{\section*{\keywordsnamegr}}{}
-\newenvironment{keywordsen}{\section*{\keywordsnameen}}{}
+\newenvironment{keywordsgr}{\section*{\keywordsnamegr}%
+  \noindent\ignorespaces}{}
+\newenvironment{keywordsen}{\section*{\keywordsnameen}%
+  \noindent\ignorespaces}{}
 \newcommand{\footacknowledgement}[1]{%
   \let\footnotesize\small%
   \let\@tmp@makefntext\@makefntext%
@@ -1423,7 +1459,7 @@
   \let\@makefntext\@tmp@makefntext%
 }
 \newenvironment{acknowledgementsgr}{%
-  \setlanguage{monogreek}%
+  \begin{greek}%
   \chapter*{\acknowledgementsnamegr}%
   \addcontentsline{toc}{chapter}{\acknowledgementsnamegr}%
   \begingroup%
@@ -1448,9 +1484,10 @@
   }
   \newpage%
   \endgroup%
+  \end{greek}%
 }
 \newenvironment{acknowledgementsen}{%
-  \selectlanguage{english}%
+  \begin{english}%
   \chapter*{\acknowledgementsnameen}%
   \addcontentsline{toc}{chapter}{\acknowledgementsnameen}%
   \begingroup%
@@ -1475,6 +1512,7 @@
   }
   \newpage%
   \endgroup%
+  \end{english}%
 }
 
 % Font customization

test.tex

@@ -11,24 +11,23 @@
 
 \frontmatter
 
-\title{Ανάπτυξη Λογισμικού για τη Μέτρηση του
-       Ηλεκτρομαγνητικού Φάσματος}
-\author{Γεώργιος Ι. Παπαδόπουλος}
-\date{Μάρτιος 1999}
-\datedefense{31}{3}{1999}
-
-\supervisor{Ιωάννης X. Παπαδάκης}
-\supervisorpos{Καθηγητής Ε.Μ.Π.}
-
-\committeeone{Ιωάννης X. Παπαδάκης}
-\committeeonepos{Καθηγητής Ε.Μ.Π.}
-\committeetwo{Νικόλαος X. Παπαδόπουλος}
-\committeetwopos{Καθηγητής Ε.Μ.Π.}
+\title{Σχεδίαση και Υλοποίηση μιας Καταπληκτικής Γλώσσας Προγραμματισμού}
+\author{Γεράσιμος Τ. Ιωάννου}
+\date{Ιούλιος 2014}
+\datedefense{17}{7}{2014}
+
+\supervisor{Νικόλαος Σ. Παπασπύρου}
+\supervisorpos{Αν. Καθηγητής Ε.Μ.Π.}
+
+\committeeone{Νικόλαος Σ. Παπασπύρου}
+\committeeonepos{Αν. Καθηγητής Ε.Μ.Π.}
+\committeetwo{Πέτρος X. Παπαδόπουλος}
+\committeetwopos{Επίκ. Καθηγητής Ε.Μ.Π.}
 \committeethree{Γεώργιος X. Νικολάου}
-\committeethreepos{Καθηγητής Ε.Μ.Π.}
+\committeethreepos{Καθηγητής Ε.Κ.Π.Α.}
 
-\department{Τομέας Συστημάτων Μετάδοσης Πληροφορίας και
-  Τεχνολογίας Υλικών}
+\TRnumber{CSD-SW-TR-42-2014}
+\department{Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών}
 
 \maketitle
 
@@ -36,33 +35,55 @@
 %%%  Abstract, in Greek
 
 \begin{abstractgr}%
-Ο σκοπός της διπλωματικής εργασίας ήταν η ανάπτυξη μεθοδολογίας
-για την ανίχνευση, αναγνώριση και καταγραφή σημάτων σε δεδομένο
-φάσμα συχνοτήτων. Η μεθοδολογία αυτή εφαρμόστηκε για την εύρεση
-παρεμβολών στο φάσμα συχνοτήτων του κυψελωτού συστήματος κινητών
-επικοινωνιών DCS 1800 στην ευρύτερη περιοχή του Λεκανοπεδίου
-Αττικής. Για το σκοπό αυτό πραγματοποιήθηκαν εξωτερικές μετρήσεις
-σε επιλεγμένα σημεία. Η επεξεργασία των μετρήσεων κατέδειξε την
-ύπαρξη παρεμβολών στο φάσμα του DCS 1800.
-
-Συγκεκριμένα, έγινε μελέτη του κυψελωτού συστήματος DCS 1800,
-παρουσιάστηκαν τα είδη παρεμβολών, παράχθηκαν σήματα DCS 1800 στο
-εργαστήριο με χρήση ψηφιακής γεννήτριας και έγινε εργαστηριακός
-έλεγχος -- εξαγωγή χαρακτηριστικών καμπυλών παθητικών (BF φίλτρο,
-ομοαξονικά καλώδια) και ενεργών στοιχείων (LNA) με χρήση HP
-Network Analyzer. Επίσης, καταγράφηκαν οι παρεμβολές σε PC μέσω
-HP Spectrum Analyzer και κατάλληλου λογισμικού.
-
-Η μεθοδολογία αυτή μπορεί να γίνει οδηγός για την πραγματοποίηση
-εξωτερικών ή εσωτερικών μετρήσεων σε οποιοδήποτε φάσμα
-συχνοτήτων, με απλές αλλαγές στις ρυθμίσεις του αναλυτή
-φάσματος. Η γενικότητα της μεθοδολογίας έγκειται στο γεγονός ότι
-έχουν καταγραφεί όλα τα βήματα, από την προστασία του προσωπικού
-και του εξοπλισμού μέχρι αναλυτικά όλα τα στάδια διεξαγωγής των
-μετρήσεων.
+  Σκοπός της παρούσας εργασίας είναι αφενός η σχεδίαση μίας απλής
+  γλώσσας υψηλού επιπέδου με υποστήριξη για προγραμματισμό με
+  αποδείξεις, αφετέρου η υλοποίηση ενός μεταγλωττιστή για τη γλώσσα
+  αυτή που θα παράγει κώδικα για μία γλώσσα ενδιάμεσου επιπέδου
+  κατάλληλη για δημιουργία πιστοποιημένων εκτελέσιμων.
+
+  Στη σημερινή εποχή, η ανάγκη για αξιόπιστο και πιστοποιημένα ασφαλή
+  κώδικα γίνεται διαρκώς ευρύτερα αντιληπτή. Τόσο κατά το παρελθόν όσο
+  και πρόσφατα έχουν γίνει γνωστά προβλήματα ασφάλειας και
+  συμβατότητας προγραμμάτων που είχαν ως αποτέλεσμα προβλήματα στην
+  λειτουργία μεγάλων συστημάτων και συνεπώς οικονομικές επιπτώσεις
+  στους οργανισμούς που τα χρησιμοποιούσαν. Τα προβλήματα αυτά
+  οφείλονται σε μεγάλο βαθμό στην έλλειψη δυνατότητας προδιαγραφής και
+  απόδειξης της ορθότητας των προγραμμάτων που χαρακτηρίζει τις
+  σύγχρονες γλώσσες προγραμματισμού. Για το σκοπό αυτό, έχουν προταθεί
+  συστήματα πιστοποιημένων εκτελέσιμων, στα οποία έχουμε τη δυνατότητα
+  να προδιαγράφουμε την ορθότητα των προγραμμάτων, και να παρέχουμε
+  μία τυπική απόδειξη αυτής, η οποία μπορεί να ελεγχθεί μηχανιστικά
+  πριν το χρόνο εκτέλεσης.
+
+  Τα συστήματα που έχουν προταθεί είναι ενδιάμεσου επιπέδου οπότε η
+  διαδικασία προγραμματισμού σε αυτά είναι ιδιαίτερα πολύπλοκη. Οι
+  γλώσσες υψηλού επιπέδου που συνοδεύουν αυτά τα συστήματα, ενώ είναι
+  ιδιαίτερα εκφραστικές, παραμένουν δύσκολες στον προγραμματισμό.  Μία
+  απλούστερη γλώσσα υψηλού επιπέδου, όπως αυτή που προτείνουμε σε αυτή
+  την εργασία, θα επέτρεπε ευρύτερη εξάπλωση του συγκεκριμένου
+  ιδιώματος προγραμματισμού.
+
+  Στη γλώσσα που προτείνουμε, ο προγραμματιστής προδιαγράφει τη μερική
+  ορθότητα του προγράμματος, δίνοντας προσυνθήκες και μετασυνθήκες για
+  τις παραμέτρους και τα αποτελέσματα των συναρτήσεων που ορίζει.
+  Επίσης δίνει ένα σύνολο θεωρημάτων βάσει του οποίου κατασκευάζονται
+  αποδείξεις της ορθής υλοποίησης και χρήσης των συναρτήσεων αυτών. Ως
+  μέρος της εργασίας, έχουμε υλοποιήσει σε γλώσσα OCaml ένα
+  μεταφραστή αυτής της γλώσσας στο σύστημα πιστοποιημένων
+  εκτελέσιμων NFLINT.
+
+  Επιτύχαμε να διατηρήσουμε τη γλώσσα κοντά στο ύφος των ευρέως
+  διαδεδομένων συναρτησιακών γλωσσών, καθώς και να διαχωρίσουμε τη
+  φάση προγραμματισμού από τη φάση απόδειξης της ορθότητας των
+  προγραμμάτων. Έτσι ένας μέσος προγραμματιστής μπορεί εύκολα να
+  προγραμματίζει στη γλώσσα που προτείνουμε με τον τρόπο που ήδη
+  γνωρίζει, και ένας γνώστης μαθηματικής λογικής να αποδεικνύει σε
+  επόμενη φάση την μερική ορθότητα των προγραμμάτων. Ως απόδειξη της
+  πρακτικότητας της προσέγγισης αυτής, παραθέτουμε ένα σύνολο
+  παραδειγμάτων στη γλώσσα με απόδειξη μερικής ορθότητας.
 \begin{keywordsgr}
-Ηλεκτρομαγνητικό φάσμα, κινητές επικοινωνίες, DCS 1800,
-εντοπισμός παρεμβολών.
+Γλώσσες προγραμματισμού, Προγραμματισμός με αποδείξεις, Ασφαλείς γλώσσες
+προγραμματισμού, Πιστοποιημένος κώδικας.
 \end{keywordsgr}
 \end{abstractgr}
 
@@ -70,34 +91,51 @@ HP Spectrum Analyzer και κατάλληλου λογισμικού.
 %%%  Abstract, in English
 
 \begin{abstracten}%
-The scope of this thesis was the development of a methodology in
-order to detect, recognize and record signals in a certain
-spectrum. This methodology was applied to the finding of
-interferences into the spectrum of the cellular mobile
-communications system DCS 1800 in the wider area of the Attika
-basin. For that purpose, outdoor measurements were carried out at
-selected sites. The processing of the measurements showed the
-existence of interferences into the DCS 1800 spectrum.
-
-Specifically, the DCS 1800 cellular system was studied and the
-interference theory was presented. Furthermore, DCS 1800 signals
-were generated at the laboratory with the use of a digital
-generator and a laboratory test - extraction of the
-characteristic curves - of passive (Bandpass Filter, co-axial
-cables) and active elements (LNA) was carried out, using a HP
-Network Analyzer. Moreover, the interferences were recorded on a
-hard disk through a HP Spectrum Analyzer and proper software.
-
-This methodology can be used as a guide for carrying out both
-outdoor and indoor measurements in any spectrum, by making simple
-changes at the function keys of the Spectrum Analyzer. The
-usefulness of the methodology is the specification of the
-procedure of the measurements in steps, from the protection of
-the personnel and the equipment up to the analytical stages of
-the measurements procedure.
+  The purpose of this diploma dissertation is on one hand the design
+  of a simple high-level language that supports programming with
+  proofs, and on the other hand the implementation of a compiler for
+  this language. This compiler will produce code for an
+  intermediate-level language suitable for creating certified
+  binaries.
+
+  The need for reliable and certifiably secure code is even more
+  pressing today than it was in the past. In many cases, security and
+  software compatibility issues put in danger the operation of large
+  systems, with substantial financial consequences. The lack of a
+  formal way of specifying and proving the correctness of programs that
+  characterizes current programming languages is one of the main reasons
+  why these issues exist. In order to address this problem, a number of
+  frameworks with support for certified binaries have recently been
+  proposed. These frameworks offer the possibility of specifying and
+  providing a formal proof of the correctness of programs. Such a proof
+  can easily be checked for validity before running the program.
+
+  The frameworks that have been proposed are intermediate-level in
+  nature, thus the process of programming in these is rather cumbersome.
+  The high-level languages that accompany some of these frameworks,
+  while very expressive, are hard to use. A simpler high-level language,
+  like the one proposed in this dissertation, would enable further use
+  of this programming idiom.
+
+  In the language we propose, the programmer specifies the partial
+  correctness of a program by annotating function definitions with pre-
+  and post-conditions that must hold for their parameters and results.
+  The programmer also provides a set of theorems, based on which proofs
+  of the proper implementation and use of the functions are constructed.
+  An implementation in OCaml of a compiler from this language to the
+  NFLINT certified binaries framework was also completed as part of this
+  dissertation.
+
+  We managed to keep the language close to the feel of the current
+  widespread functional languages, and also to fully separate the
+  programming stage from the correctness-proving stage. Thus an average
+  programmer can program in a familiar way in our language, and later an
+  expert on formal logic can prove the semi-correctness of a program.
+  As evidence of the practicality of our design, we provide a number of
+  examples in our language with full semi-correctness proofs.
 \begin{keywordsen}
-Electromagnetic spectrum, cellular mobile communications, DCS
-1800, interference detection.
+Programming languages, Programming with proofs, Secure programming
+languages, Certified code.
 \end{keywordsen}
 \end{abstracten}
 
@@ -308,6 +346,14 @@ Electromagnetic spectrum, cellular mobile communications, DCS
 
 $A \rightarrow B$ : συνάρτηση από το πεδίο $A$ στο πεδίο $B$.
 
+\chapter{Ευρετήριο γλωσσών}
+
+\textbf{Haskell} : η γλώσσα της ζωής μου.
+
+\chapter{Ευρετήριο αριθμών}
+
+42 : life, the universe and everything.
+
 
 %%%  End of document