Κύριος ερευνητής Hongwei Xi
Οι φοιτητές Chiyan Chen (απόφοιτος), Sa Cui (απόφοιτος), Likai Liu (προπτυχιακό), Rui Shi (απόφοιτος), Dengping Zhu (απόφοιτος)
Υποστήριξη NSF CCR-0224244, 2000 – 2004
Λέξεις-κλειδιά εξαρτημένοι τύποι, επιτακτικός προγραμματισμός, Xanadu, DTAL
Προτείνουμε να εμπλουτίσουμε τον πρακτικό επιτακτικό προγραμματισμό με μια πειθαρχία τύπου που επιτρέπει την εξειδίκευση και εξαγωγή αξιόπιστων πληροφοριών σχετικά με τα προγράμματα από εκείνες που επιβάλλονται σε γλώσσες όπως Java και Standard ML (SML).
Το κύριο κίνητρο για την ανάπτυξη μιας τέτοιας πειθαρχίας τύπου είναι να επιτρέψει στον προγραμματιστή να εκφράσει περισσότερες ιδιότητες προγράμματος με τύπους και στη συνέχεια να επιβάλει αυτές τις ιδιότητες μέσω του ελέγχου τύπου. Είναι γνωστό ότι μια πειθαρχία τύπου όπως αυτή που επιβάλλεται σε Java ή SML μπορεί να διευκολύνει αποτελεσματικά την ανίχνευση σφαλμάτων προγράμματος. Επομένως, μπορεί να αναμένεται ότι μια ισχυρότερη πειθαρχία τύπου μπορεί να βοηθήσει στην ανίχνευση περισσότερων σφαλμάτων προγράμματος, οδηγώντας στην παραγωγή πιο ισχυρού λογισμικού.
Σε γενικές γραμμές, υπάρχουν δύο κατευθύνσεις για την επέκταση ενός συστήματος στυλ τύπου Hindley-Milner όπως το σύστημα του SML. Το ένα είναι να το επεκτείνουμε έτσι ώστε να μπορούν να γίνουν δεκτά περισσότερα προγράμματα ως ορθά για τον τύπο και το άλλο να επεκταθεί έτσι ώστε τα προγράμματα να μπορούν να αποδίδονται με ακριβέστερους τύπους. Μας ενδιαφέρει κυρίως η τελευταία.
Η έννοια των εξαρτώμενων τύπων, η οποία ευρέως εφευρέθηκε για τη μοντελοποίηση προγραμμάτων με μεγαλύτερη ακρίβεια, έχει μελετηθεί για τουλάχιστον τρεις δεκαετίες. Ωστόσο, η χρήση εξαρτώμενων τύπων στον πρακτικό προγραμματισμό είναι σπάνια αν υπάρχει, και αυτό, νομίζουμε, οφείλεται κυρίως σε κάποια μεγάλη δυσκολία στο σχεδιασμό ενός πρακτικά χρήσιμου αλγορίθμου συμπερασμάτων για ένα σύστημα εξαρτώμενου τύπου. Έχουμε παρουσιάσει μια προσέγγιση για την αντιμετώπιση της δυσκολίας στο σχεδιασμό του Dependent ML (DML), το οποίο επεκτείνει το ML με μια έννοια περιορισμένης μορφής εξαρτώμενων τύπων. Επίσης, αποδεικνύεται ότι οι εξαρτώμενοι τύποι στη DML μπορούν να διευκολύνουν την εξάλειψη της συσχέτισης που συνδέεται με τη συστοιχία, την απομάκρυνση της ρήτρας αντιστοίχισης μοτίβων, την εξάλειψη της ετικέτας και την απεικόνιση των σημείων δεδομένων. Προφανώς, ένα άμεσο ερώτημα είναι εάν μπορούμε να αποκομίσουμε κάποια παρόμοια οφέλη με την ενσωμάτωση εξαρτημένων τύπων σε επιτακτικό προγραμματισμό. Προτείνουμε να αντιμετωπίσουμε αυτό το ερώτημα σχεδιάζοντας μια γλώσσα προγραμματισμού που εξαρτάται από την πληκτρολόγηση.
Υπάρχει ακόμα ένα κίνητρο για την ενσωμάτωση εξαρτημένων τύπων σε πρακτικό προγραμματισμό. Σε ένα μη αξιόπιστο περιβάλλον υπολογιστών, όπως το Internet, ο κινητός κώδικας που λαμβάνεται από άγνωστη πηγή μπορεί να μην είναι αξιόπιστος. Ως εκ τούτου, ο παραλήπτης κώδικα πρέπει συχνά να εκτελεί συγκεκριμένους στατικούς και / ή δυναμικούς ελέγχους στον παραλαμβανόμενο κώδικα για κινητά, για να αποτρέψει την εμφάνιση κάποιων ανεπιθύμητων συνεπειών όπως παραβίαση της ασφάλειας. Έχουμε σχεδιάσει μια γλώσσα συναρμολόγησης εξαρτημένης γλώσσας (DTAL), στην οποία το σύστημα τύπου μπορεί να εγγυηθεί την ασφάλεια μνήμης του κώδικα DTAL, όπου η ασφάλεια μνήμης αποτελείται τόσο από την ασφάλεια τύπου όσο και από την ασφαλή καταγραφή των συστοιχιών. Ωστόσο, είναι δύσκολο να καταρτιστεί κώδικας DTAL σε πρόγραμμα γραμμένο σε γλώσσα όπως η Java, καθώς συχνά φαίνεται αναποτελεσματικό να συνθέσουμε από ένα τέτοιο πρόγραμμα τις πληροφορίες τύπου που χρειάζονται στον κώδικα DTAL. Με μια εξειδικευμένη γλώσσα προγραμματισμού που εξαρτάται από την πληκτρολόγηση, αναμένουμε να εφαρμόσουμε έναν μεταγλωττιστή που μπορεί να μεταφράζει εξαρτημένους τύπους σε επίπεδο πηγής σε εξαρτώμενους τύπους σε επίπεδο συναρμολόγησης, παράγοντας αποτελεσματικά τον κωδικό DTAL.
Εν ολίγοις, προτείνουμε να σχεδιάσουμε μια γλώσσα προγραμματισμού που εξαρτάται από την πληκτρολόγηση, για τη μελέτη της χρήσης εξαρτώμενων τύπων στον πρακτικό επιτακτικό προγραμματισμό τόσο σε επίπεδο πηγής όσο και σε επίπεδο συναρμολόγησης. Αναμένουμε ότι αυτή η μελέτη μπορεί τελικά να οδηγήσει στην παραγωγή λογισμικού που δεν είναι μόνο πιο ισχυρό αλλά και λιγότερο δαπανηρό για να διατηρηθεί.
Proteínoume na emploutísoume ton praktikó epitaktikó programmatismó me mia peitharchía týpou pou epitrépei tin exeidíkefsi kai exagogí axiópiston pliroforión schetiká me ta prográmmata apó ekeínes pou epivállontai se glósses ópos Java kai Standard ML (SML).
To kýrio kínitro gia tin anáptyxi mias tétoias peitharchías týpou eínai na epitrépsei ston programmatistí na ekfrásei perissóteres idiótites prográmmatos me týpous kai sti synécheia na epiválei aftés tis idiótites méso tou elénchou týpou. Eínai gnostó óti mia peitharchía týpou ópos aftí pou epiválletai se Java í SML boreí na diefkolýnei apotelesmatiká tin aníchnefsi sfalmáton prográmmatos. Epoménos, boreí na anaménetai óti mia ischyróteri peitharchía týpou boreí na voithísei stin aníchnefsi perissóteron sfalmáton prográmmatos, odigóntas stin paragogí pio ischyroú logismikoú.
Se genikés grammés, ypárchoun dýo katefthýnseis gia tin epéktasi enós systímatos styl týpou Hindley-Milner ópos to sýstima tou SML. To éna eínai na to epekteínoume étsi óste na boroún na gínoun dektá perissótera prográmmata os orthá gia ton týpo kai to állo na epektatheí étsi óste ta prográmmata na boroún na apodídontai me akrivésterous týpous. Mas endiaférei kyríos i teleftaía.
I énnoia ton exartómenon týpon, i opoía evréos efevréthike gia ti montelopoíisi programmáton me megalýteri akríveia, échei meletitheí gia touláchiston treis dekaetíes. Ostóso, i chrísi exartómenon týpon ston praktikó programmatismó eínai spánia an ypárchei, kai aftó, nomízoume, ofeíletai kyríos se kápoia megáli dyskolía sto schediasmó enós praktiká chrísimou algoríthmou symperasmáton gia éna sýstima exartómenou týpou. Échoume parousiásei mia proséngisi gia tin antimetópisi tis dyskolías sto schediasmó tou Dependent ML (DML), to opoío epekteínei to ML me mia énnoia periorisménis morfís exartómenon týpon. Epísis, apodeiknýetai óti oi exartómenoi týpoi sti DML boroún na diefkolýnoun tin exáleipsi tis syschétisis pou syndéetai me ti systoichía, tin apomákrynsi tis rítras antistoíchisis motívon, tin exáleipsi tis etikétas kai tin apeikónisi ton simeíon dedoménon. Profanós, éna ámeso erótima eínai eán boroúme na apokomísoume kápoia parómoia oféli me tin ensomátosi exartiménon týpon se epitaktikó programmatismó. Proteínoume na antimetopísoume aftó to erótima schediázontas mia glóssa programmatismoú pou exartátai apó tin pliktrológisi.
Ypárchei akóma éna kínitro gia tin ensomátosi exartiménon týpon se praktikó programmatismó. Se éna mi axiópisto perivállon ypologistón, ópos to Internet, o kinitós kódikas pou lamvánetai apó ágnosti pigí boreí na min eínai axiópistos. Os ek toútou, o paralíptis kódika prépei sychná na ekteleí synkekriménous statikoús kai / í dynamikoús elénchous ston paralamvanómeno kódika gia kinitá, gia na apotrépsei tin emfánisi kápoion anepithýmiton synepeión ópos paravíasi tis asfáleias. Échoume schediásei mia glóssa synarmológisis exartiménis glóssas (DTAL), stin opoía to sýstima týpou boreí na engyitheí tin asfáleia mnímis tou kódika DTAL, ópou i asfáleia mnímis apoteleítai tóso apó tin asfáleia týpou óso kai apó tin asfalí katagrafí ton systoichión. Ostóso, eínai dýskolo na katartisteí kódikas DTAL se prógramma gramméno se glóssa ópos i Java, kathós sychná faínetai anapotelesmatikó na synthésoume apó éna tétoio prógramma tis pliroforíes týpou pou chreiázontai ston kódika DTAL. Me mia exeidikevméni glóssa programmatismoú pou exartátai apó tin pliktrológisi, anaménoume na efarmósoume énan metaglottistí pou boreí na metafrázei exartiménous týpous se epípedo pigís se exartómenous týpous se epípedo synarmológisis, parágontas apotelesmatiká ton kodikó DTAL.
En olígois, proteínoume na schediásoume mia glóssa programmatismoú pou exartátai apó tin pliktrológisi, gia ti meléti tis chrísis exartómenon týpon ston praktikó epitaktikó programmatismó tóso se epípedo pigís óso kai se epípedo synarmológisis. Anaménoume óti aftí i meléti boreí teliká na odigísei stin paragogí logismikoú pou den eínai móno pio ischyró allá kai ligótero dapaniró gia na diatiritheí.
Τι είναι το Xanadu;
Το Xanadu είναι μια γλώσσα προγραμματισμού που εξαρτάται από την πληκτρολόγηση. Ακολουθεί μια σύντομη εισαγωγή (ppt).
Παραδείγματα προγράμματος στο Xanadu:
Παρουσιάζουμε ορισμένα ρεαλιστικά παραδείγματα στο Xanadu για να υποστηρίξουμε την πρακτικότητα του Xanadu.
- Δυαδική αναζήτηση:
Τα παρακάτω είναι μια εφαρμογή της δυαδικής αναζήτησης σε έναν ακέραιο πίνακα στο Xanadu. Η καινοτομία στην υλοποίηση είναι ο σχολιασμός που ακολουθεί τη λέξη-κλειδί αμετάβλητη. Αυτός ο σχολιασμός είναι ένας εξαρτώμενος τύπος που επιβεβαιώνει ορισμένες πληροφορίες στο σημείο εισόδου του βρόχου. Σε αυτή την περίπτωση, ο σχολιασμός δηλώνει ότι οι μεταβλητές χαμηλής και υψηλής έχουν τύπους int (i) και int (j) στο σημείο εισόδου του βρόχου για ορισμένους ακέραιους αριθμούς i και j έτσι ώστε και οι 0 <= i <= n και 0 < 1 <= n κρατήστε πατημένο. Αυτός είναι ένας βρόχος αμετάβλητος, ο οποίος μπορεί να εγγυηθεί ότι η λειτουργία του δείκτη array [mid] στο σώμα του βρόχου είναι ασφαλής, δηλαδή δεν μπορεί ποτέ να βγει από τα όρια. Το κρίσιμο σημείο είναι ότι ο έλεγχος τύπου στο Xanadu μπορεί να ελέγξει αυτόματα αν ένα πρόγραμμα αμετάβλητο όπως αυτό που παρέχεται από τον προγραμματιστή είναι πράγματι ένα σωστό πρόγραμμα αμετάβλητο.
Επιπλέον, ελέγχεται αυτόματα στο Xanadu αν μια μεταβλητή έχει ήδη αρχικοποιηθεί πριν διαβαστεί.
{n:nat}
int bsearch(key: int, vec[n]: int) {
var: int low, mid, high;
int x;;
low = 0; high = arraysize(vec) – 1;
invariant:
[i:int, j:int | 0 <= i <= n, 0 <= j+1 <= n] (low: int(i), high: int(j))
while (low <= high) {
mid = (low + high) / 2;
x = vec[mid];
if (key == x) { return mid; }
else if (key < x) { high = mid – 1; }
else { low = mid + 1; }
}
return -1;
}
- Λίστα Αντίστροφη:
Αυτό το παράδειγμα καταδεικνύει ότι μπορεί να επαληθευτεί στο σύστημα τύπου του Xanadu ότι η λειτουργία ανάστροφης λίστας διατηρεί το μήκος.
Η ακόλουθη δήλωση δηλώνει μια λίστα πολυμορφικών συνενώσεων <‘a>. Οι δύο κατασκευαστές Nil και μειονεκτήματα που σχετίζονται με τον τύπο συνένσης είναι οι τύποι <a> (0) και {n: nat} ‘a * <‘ a> λίστα (n) -> <‘a> ), αντίστοιχα, που σημαίνει ότι το Nil είναι ένας κατάλογος με το μήκος 0 και τα Ημίσκληρα επιστρέφει μια λίστα μήκους n +! όταν δίνεται ένα στοιχείο και ένας κατάλογος μήκους n. Σημειώστε ότι το {n: nat} υποδεικνύει ότι το n, μια μεταβλητή δείκτη τύπου της nat nat, είναι γενικά ποσοτικοποιημένη. nat είναι το είδος ενός δείκτη τύπου που αντιπροσωπεύει έναν φυσικό αριθμό.
Αυτό το παράδειγμα καταδεικνύει ότι μπορεί να επαληθευτεί στο σύστημα τύπου του Xanadu ότι η λειτουργία ανάστροφης λίστας διατηρεί το μήκος.
Η ακόλουθη δήλωση δηλώνει μια λίστα πολυμορφικών συνενώσεων <‘a>. Οι δύο κατασκευαστές Nil και μειονεκτήματα που σχετίζονται με τον τύπο συνένσης είναι οι τύποι <a> (0) και {n: nat} ‘a * <‘ a> λίστα (n) -> <‘a> ), αντίστοιχα, που σημαίνει ότι το Nil είναι ένας κατάλογος με το μήκος 0 και τα Ημίσκληρα επιστρέφει μια λίστα μήκους n +! όταν δίνεται ένα στοιχείο και ένας κατάλογος μήκους n. Σημειώστε ότι το {n: nat} υποδεικνύει ότι το n, μια μεταβλητή δείκτη τύπου της nat nat, είναι γενικά ποσοτικοποιημένη. nat είναι το είδος ενός δείκτη τύπου που αντιπροσωπεύει έναν φυσικό αριθμό.
union <‘a> list with nat {
Nil(0);
{n:nat} Cons(n+1) of ‘a * <‘a> list(n)
}
Τα παρακάτω εφαρμόζουν τη λειτουργία αντίστροφης προσάρτησης σε λίστες. Η κεφαλίδα της συνάρτησης δηλώνει ότι για τους φυσικούς αριθμούς m και n, η rev_app παίρνει ένα ζευγάρι λιστών μήκους m και n και επιστρέφει μια λίστα μήκους m + n. Είναι σαφές ότι η έξοδος, που σημαίνει ότι ένα πρόγραμμα σταματάει ασυνήθιστα, δεν μπορεί ποτέ να εκτελεστεί κατά το χρόνο εκτέλεσης και ως εκ τούτου περιττό στην περίπτωση. Δυστυχώς, αυτές οι πληροφορίες δεν μπορούν να ληφθούν στο σύστημα τύπου του Xanadu.
(‘a){m:nat, n:nat}
<‘a> list(m+n) rev_app
(xs: <‘a> list(m), ys: <‘a> list(n)) {
var: ‘a x;;
invariant:
[m1:nat,n1:nat | m1+n1 = m+n] (xs: <‘a> list(m1), ys: <‘a> list(n1))
while (true) {
switch (xs) {
case Nil: return ys;
case Cons(x, xs): ys = Cons(x, ys);
}
}
exit;
}
Η λειτουργία ανάστροφης λίστας μπορεί τώρα να εφαρμοστεί ως εξής. Η κεφαλίδα της λειτουργίας δηλώνει ότι πρόκειται για λειτουργία συντήρησης μήκους.
(‘a){n:nat}
<‘a> list(n) reverse (xs: <‘a> list(n)) {
return rev_app (xs, Nil);
}
- Πολλαπλασιασμός σειράς αραιών γραμμών:
Εφαρμόζουμε τον πολλαπλασιασμό μεταξύ μιας αραιής συστοιχίας και ενός διανύσματος. Ορίζουμε ένα πολυμορφικό αρχείο <‘a> sparseArray για την αναπαράσταση δύο διαστάσεων αραιών συστοιχιών στις οποίες κάθε στοιχείο είναι τύπου’ a. Το sparseArray είναι ευρετηριασμένο με ένα ζευγάρι φυσικών αριθμών (m, n), που αντιπροσωπεύουν τον αριθμό των σειρών και τον αριθμό των στηλών σε μια αραιή σειρά, αντίστοιχα. Ας είναι μια εγγραφή τύπου <‘a> sparseArray (m, n). Στη συνέχεια, τα sa έχουν τρία στοιχεία, δηλαδή σειρά, col και δεδομένα. Σαφώς, οι τύποι που έχουν εκχωρηθεί στη σειρά και στη στήλη υποδεικνύουν ότι οι sa και sa.col επιστρέφουν τις διαστάσεις του sa Ο τύπος που αντιστοιχεί στα δεδομένα δηλώνει ότι το sa.data είναι ένας πίνακας μεγέθους m. Σε αυτή τη συστοιχία, κάθε στοιχείο, το οποίο αντιπροσωπεύει μια σειρά σε μια αραιή συστοιχία, είναι ένας κατάλογος ζευγών και κάθε ζεύγος αποτελείται από έναν φυσικό αριθμό μικρότερο από το n και ένα στοιχείο του τύπου «α».
{m:nat,n:nat}
record <‘a> sparseArray(m, n) {
row: int(m);
col: int(n);
data[m]: <int[0,n) * ‘a> list
}
Η συνάρτηση mat_vec_mult παίρνει μια διακεκομμένη διάταξη διαστάσεων (m, n) και ένα διάνυσμα σημείου float μεγέθους n και μια επισήμανση διανύσματος float point μεγέθους m. Σημειώστε ότι η συνάρτηση list_vec_mult χρησιμοποιείται για τον υπολογισμό του κουκκιδωτού προϊόντος μιας γραμμής στην αραιή συστοιχία και το διάνυσμα. Το σημείο που κάνουμε είναι ότι το σύστημα τύπου του Xanadu μπορεί να εγγυηθεί ότι όλες οι πράξεις υπογραφής του πίνακα σε αυτό το παράδειγμα είναι ασφαλείς κατά την εκτέλεση.
{n:nat}
float
list_vec_mult (xs: <int[0,n) * float> list, vec[n]: float) {
var: int i; float f, sum;;
sum = 0.0;
while (true) {
switch (xs) {
case Nil: return sum;
case Cons((i, f), xs): sum = sum +. f *. vec[i];
}
}
exit;
}
{m:nat,n:nat}
<float> array(m)
mat_vec_mult(mat: <float> sparseArray(m, n), vec[n]: float) {
var: nat i; float result[];;
result = newarray(mat.row, 0.0);
for (i = 0; i < mat.row; i = i + 1) {
result[i] = list_vec_mult (mat.data[i], vec);
}
return result;
}
- Heapsort:
Θα μπορούσατε να το καταλάβετε μόνοι σας 🙂
{max:nat}
record <‘a> heap(max) {
max: int(max);
mutable size: [size:nat | size <= max] int(size);
data[max]: ‘a
}
max:nat, i:nat | i < max}
unit heapify (heap: <float> heap(max), i: int(i)) {
var: int size, left, right;
float temp;
largest: [a:nat | a < max] int(a) ;;
left = 2 * i + 1; right = 2 * i + 2;
size = heap.size; largest = i;
if (left < size) {
if (heap.data[left] >. heap.data[i]) { largest = left; }
}
if (right < size) {
if (heap.data[right] >. heap.data[largest]) { largest = right; }
}
if (largest <> i) {
temp = heap.data[i];
heap.data[i] = heap.data[largest];
heap.data[largest] = temp;
heapify (heap, largest);
}
}
{max:nat}
unit buildheap (heap: <float> heap(max)) {
var: int i, size;;
size = heap.size;
invariant: [i:int | i < max] (i: int(i))
for (i = size / 2 – 1; i >= 0; i = i – 1) {
heapify (heap, i);
}
}
{max:nat}
unit heapsort (heap: <float> heap(max)) {
var: int size, i; float temp;;
buildheap (heap);
invariant: [i:int | i < max] (i: int(i))
for (i = heap.max – 1; i >= 1; i = i – 1) {
temp = heap.data[i];
heap.data[i] = heap.data[0];
heap.data[0] = temp;
heap.size = i;
heapify(heap, 0);
}
}
- Gaussian Εξάλειψη:
Θα μπορούσατε να το καταλάβετε μόνοι σας 🙂
{m:nat, n:nat}
record <‘a> matrix(m,n) {
row: int(m);
col: int(n);
data[m][n]: ‘a
}
{m:nat,n:nat,i:nat,j:nat | i < m, j < m}
unit
rowSwap(data[m][n]: float, i:int(i), j:int(j)) {
var: temp[]: float;;
temp = data[i];
data[i] = data[j];
data[j] = temp;
}
{n:nat,i:nat | i < n}
unit
norm(r[n]: float, n:int(n), i:int(i)) {
var: float x;;
x = r[i]; r[i] = 1.0; i = i + 1;
invariant: [i:nat] (i: int(i))
while (i < n) { r[i] = r[i] /. x; i = i + 1;}
}
{n:nat, i:nat | i < n}
unit
rowElim(r[n]: float, s[n]: float, n:int(n), i: int(i)) {
var: float x;;
x = s[i]; s[i] = 0.0; i = i + 1;
invariant: [i:nat] (i: int(i))
while (i < n) { s[i] = s[i] -. x *. r[i]; i = i + 1;}
}
{m:nat, n:nat, i:nat | m > i, n > i}
[k:nat | k < m] int(k)
rowMax (data[m][n]: float, m: int(m), i: int(i)) {
var: nat j; float x, y;
max: [k: nat | k < m] int(k);;
max = i; x = fabs(data[i][i]); j = i + 1;
while (j < m) {
y = fabs(data[j][i]);
if (y >. x) { x = y; max = j; }
j = j + 1;
}
return max;
}
{n:nat | n > 0}
unit gauss (mat: <float> matrix(n,n+1)) {
var: float data[][n+1]; nat i, j, max, n;;
data = mat.data; n = mat.row;
for (i = 0; i < n; i = i + 1) {
max = rowMax(data, n, i);
norm (data[max], n+1, i);
rowSwap(data, i, max);
for (j = i + 1; j < n; j = j + 1) {
rowElim(data[i], data[j], n+1, i);
}
}
}
- Περισσότερα Παραδείγματα:
Βρείτε εδώ και περισσότερα παραδείγματα.
Έγγραφα που σχετίζονται ή σχετίζονται με το Xanadu
- Hongwe Xi, διευκόλυνση της επαλήθευσης του προγράμματος με εξαρτώμενους τύπους, Δεκέμβριος 1999. (σχέδιο)
- Hongwe Xi, Προγραμματισμός με Εξαρτημένους Τύπους, Δεκέμβριος 1999. (σχέδιο) (εκτεταμένη περίληψη)
- Hongwei Xi και Robert Harper, γλώσσα συνηθισμένου πληκτρολογίου, τεχνική έκθεση OGI-CSE-99-008, Ιούλιος 1999. (bibtex) (ps) (pdf) (εκτεταμένη περίληψη)
- Διαφάνειες
Μια συζήτηση για το Xanadu μπορεί να βρεθεί εδώ
- Εκτέλεση
Μια μη πρωτότυπη υλοποίηση του Xanadu μπορεί να βρεθεί εδώ. Κρατήστε συντονισμένο.
Link to original source:http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html
