Commit d8355078 authored by Pietro Abate's avatar Pietro Abate

- clean up legacy website and debian directory

- the web directory now contains only the cgi code
parent 70331ae3
Document: cduce
Title: CDuce documentation
Author: The CDuce Team (http://www.cduce.org/team.html)
Abstract: Local copy of the CDuce website including tutorial, users'manual and examples
Section: interpreters
Format: HTML
Index: /usr/share/doc/cduce/html/index.html
Files: /usr/share/doc/cduce/html/*.html
cduce usr/bin/
dtd2cduce usr/bin/
debian/tmp/usr/bin/* usr/bin/
debian/tmp/usr/share/* usr/share/
cduce (0.1.1-1) unstable; urgency=low
* New upstream release
- Various bug fixes (expat might now work)
- Sequencing operator e1;e2 (equivalent to: let [] = e1 in e2)
- Encoded references
-- Stefano Zacchiroli <zack@debian.org> Sun, 14 Sep 2003 11:50:59 +0200
cduce (0.1.0-1) unstable; urgency=low
* Initial Release.
-- Stefano Zacchiroli <zack@debian.org> Fri, 4 Jul 2003 15:17:41 +0200
Source: cduce
Section: interpreters
Priority: optional
Maintainer: Stefano Zacchiroli <zack@debian.org>
Build-Depends: debhelper (>> 4.0.0), dpatch, ocaml-3.07, ocaml-findlib, libwlexing-ocaml-dev, libpcre-ocaml-dev, libocamlnet-ocaml-dev, libpxp-ocaml-dev, libexpat1-dev
Standards-Version: 3.6.1.0
Package: cduce
Architecture: any
Depends: ${shlibs:Depends} ${misc:Depends}
Description: programming language adapted to the manipulation of XML data
CDuce is a modern programming language adapted to the manipulation of XML
documents.
.
Some of CDuce peculiar features:
- XML objects can be manipulated as first-class citizen values: elements,
sequences, tags, characters and strings, attribute sets; sequences of XML
elements can be specified by regular expressions, which also apply to
characters strings;
- functions themselves are first-class values, they can be manipulated,
stored in data structure, returned by a function, ...;
- a powerful pattern matching operation can perform complex extractions from
sequences of XML elements;
- a rich type algebra, with recursive types and arbitrary boolean
combinations (union, intersection, complement) allows precise definitions
of data structures and XML types; general purpose types and types
constructors are taken seriously (products, extensible records, arbitrary
precision integers with interval constraints, Unicode characters);
- polymorphism through a natural notion of subtyping, and overloaded
functions with dynamic dispatch;
- an highly-effective type-driven compilation schema
.
CDuce is fast, functional, type-safe, and conforms to basic standards:
Unicode, XML, DTD, Namespaces are fully supported, partial support of XML
Schema validation is in alpha testing (and undocumented) while queries are
being implemented.
This package was debianized by Stefano Zacchiroli <zack@debian.org> on
Fri, 4 Jul 2003 15:17:41 +0200.
It was downloaded from:
http://www.cduce.org/download.html
The main author of CDuce is:
Alain Frisch <Alain.Frisch@ens.fr>
with contributions of the CDuce Team (http://www.cduce.org/team.html):
CDuce @ ENS (Paris)
* Giuseppe Castagna <Giuseppe.Castagna@ens.fr> (CNRS researcher)
* Alain Frisch <Alain.Frisch@ens.fr> (Ph.D. student)
* Stefano Zacchiroli <zack@bononia.it> (Graduate student)
* Josh de Letaillade <delatail@clipper.ens.fr> (DEA student)
CDuce @ LRI (Orsay)
* Véronique Benzaken <veronique.benzaken@.lri.fr> (Prof. Univ. Paris 11)
* Marwan Burelle <Marwan.Burelle@lri.fr> (Ph.D student)
* Cédric Miachon <miachon@lri.fr> (DEA student)
Copyright:
The CDuce interpreter is distributed under the terms of the Q Public License
version 1.0 (included below). The "Choice of Law" section been modified
from the original Q Public License (Copyright (C) 1999 Troll Tech AS, Norway).
----------------------------------------------------------------------
THE Q PUBLIC LICENSE version 1.0
Copyright (C) 1999 Troll Tech AS, Norway.
Everyone is permitted to copy and
distribute this license document.
The intent of this license is to establish freedom to share and change
the software regulated by this license under the open source model.
This license applies to any software containing a notice placed by the
copyright holder saying that it may be distributed under the terms of
the Q Public License version 1.0. Such software is herein referred to
as the Software. This license covers modification and distribution of
the Software, use of third-party application programs based on the
Software, and development of free software which uses the Software.
Granted Rights
1. You are granted the non-exclusive rights set forth in this license
provided you agree to and comply with any and all conditions in this
license. Whole or partial distribution of the Software, or software
items that link with the Software, in any form signifies acceptance of
this license.
2. You may copy and distribute the Software in unmodified form
provided that the entire package, including - but not restricted to -
copyright, trademark notices and disclaimers, as released by the
initial developer of the Software, is distributed.
3. You may make modifications to the Software and distribute your
modifications, in a form that is separate from the Software, such as
patches. The following restrictions apply to modifications:
a. Modifications must not alter or remove any copyright notices
in the Software.
b. When modifications to the Software are released under this
license, a non-exclusive royalty-free right is granted to the
initial developer of the Software to distribute your
modification in future versions of the Software provided such
versions remain available under these terms in addition to any
other license(s) of the initial developer.
4. You may distribute machine-executable forms of the Software or
machine-executable forms of modified versions of the Software,
provided that you meet these restrictions:
a. You must include this license document in the distribution.
b. You must ensure that all recipients of the machine-executable
forms are also able to receive the complete machine-readable
source code to the distributed Software, including all
modifications, without any charge beyond the costs of data
transfer, and place prominent notices in the distribution
explaining this.
c. You must ensure that all modifications included in the
machine-executable forms are available under the terms of this
license.
5. You may use the original or modified versions of the Software to
compile, link and run application programs legally developed by you or
by others.
6. You may develop application programs, reusable components and other
software items that link with the original or modified versions of the
Software. These items, when distributed, are subject to the following
requirements:
a. You must ensure that all recipients of machine-executable
forms of these items are also able to receive and use the
complete machine-readable source code to the items without any
charge beyond the costs of data transfer.
b. You must explicitly license all recipients of your items to
use and re-distribute original and modified versions of the
items in both machine-executable and source code forms. The
recipients must be able to do so without any charges whatsoever,
and they must be able to re-distribute to anyone they choose.
c. If the items are not available to the general public, and the
initial developer of the Software requests a copy of the items,
then you must supply one.
Limitations of Liability
In no event shall the initial developers or copyright holders be
liable for any damages whatsoever, including - but not restricted to -
lost revenue or profits or other direct, indirect, special, incidental
or consequential damages, even if they have been advised of the
possibility of such damages, except to the extent invariable law, if
any, provides otherwise.
No Warranty
The Software and this license document are provided AS IS with NO
WARRANTY OF ANY KIND, INCLUDING THE WARRANTY OF DESIGN,
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
Choice of Law
This license is governed by the Laws of France. Disputes shall be
settled by the Court of Paris.
#!/bin/sh -e
## 01_makefile_conf.dpatch by Stefano Zacchiroli <zack@debian.org>
##
## All lines beginning with `## DP:' are a description of the patch.
## DP: installs HTML documentation and CGIs in debian specific dirs
if [ $# -ne 1 ]; then
echo >&2 "`basename $0`: script expects -patch|-unpatch as argument"
exit 1
fi
[ -f debian/patches/00patch-opts ] && . debian/patches/00patch-opts
patch_opts="${patch_opts:--f --no-backup-if-mismatch}"
case "$1" in
-patch) patch $patch_opts -p1 < $0;;
-unpatch) patch $patch_opts -p1 -R < $0;;
*)
echo >&2 "`basename $0`: script expects -patch|-unpatch as argument"
exit 1;;
esac
exit 0
@DPATCH@
diff -urNad /home/zack/dati/cduce/CDUCE.main/Makefile.conf CDUCE.main/Makefile.conf
--- /home/zack/dati/cduce/CDUCE.main/Makefile.conf 2004-01-11 14:15:28.000000000 +0100
+++ CDUCE.main/Makefile.conf 2004-01-11 14:25:18.000000000 +0100
@@ -1,4 +1,5 @@
# build CDuce using OCaml native code compiler
+# DEBIAN: overridden in debian/rules
ifeq ($(NATIVE), false)
else
NATIVE = true
@@ -26,7 +27,7 @@
# Customize the following variables to match the settings
# of your local web server
-WEB_PREFIX = /var/www
-CGI_DIR = $(WEB_PREFIX)/cgi-bin
+WEB_PREFIX = debian/tmp/usr/share/doc/cduce
+CGI_DIR = debian/tmp/usr/lib/cgi-bin
HTML_DIR = $(WEB_PREFIX)/html
SESSION_DIR = /tmp/cduce_sessions
#!/usr/bin/make -f
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
include /usr/share/dpatch/dpatch.make
# This has to be exported to make some magic below work.
export DH_OPTIONS
MAKE_OPTS := $(shell if [ -x /usr/bin/ocamlopt ]; then echo "NATIVE=true"; else echo "NATIVE=false"; fi)
#Architecture
build: build-arch
build-arch: build-arch-stamp
build-arch-stamp: patch-stamp
$(MAKE) $(MAKE_OPTS) all
touch build-arch-stamp
clean: patch clean1 unpatch
clean1:
dh_testdir
dh_testroot
rm -f build-arch-stamp
# Add here commands to clean up after the build process.
-$(MAKE) $(MAKE_OPTS) clean
dh_clean
install: install-arch
install-arch:
dh_testdir
dh_testroot
dh_clean -k -a
dh_installdirs -a
mkdir -p debian/tmp/usr/bin
mkdir -p debian/tmp/usr/lib/cgi-bin/cduce
mkdir -p debian/tmp/usr/share/doc/cduce/html
$(MAKE) $(MAKE_OPTS) install_web
dh_install -a
binary-common:
dh_testdir
dh_testroot
dh_installchangelogs CHANGES
dh_installdocs
dh_installexamples
dh_installman doc/cduce.1
dh_link
dh_strip
dh_compress
dh_fixperms
dh_installdeb
dh_shlibdeps
dh_gencontrol
dh_md5sums
dh_builddeb
binary-arch: build-arch install-arch
$(MAKE) -f debian/rules DH_OPTIONS=-a binary-common
binary: binary-arch
.PHONY: build clean binary-arch binary install install-arch
<?xml version="1.0" encoding="ISO-8859-1" standalone="yes"?>
<page name="CompteRendus">
<title>Compte Rendus</title>
<left>
<boxes-toc/>
</left>
<box title="Compte-Rendu de la réunion du 14/10/04" link="141004">
Présents:<ul>
<li> Alain Frisch</li>
<li> Guillaume Gillard</li>
<li> Giuseppe Castagna</li>
<li> Cédric Miachon</li>
</ul>
<ol>
<li> Discussion autour de l'implantation du système de type dans l'atelier Brixlogix;
implantation en cours en Java du typecheker.
Les types CDuce sont idéaux pour le traitement global des données, et pour aller au-delà de la vérification de protocoles.
Le type singleton est intéressant pour les flots de contrôle, mais l'union pose problème.
</li>
<li>
L'objectif de l'atelier est de typer le document de sortie, le problème se pose sur le typage de l'impératif
nottamment pour l'aliasing.
Il faudrait mieux typer le programme CDuce correspondant à l'atelier, par le typage de chaque brique par un programme CDuce.
</li>
<li>
Discussion autour d'un logiciel pour le langage de requêtes de CDuce, en rapport avec l'atelier.
</li>
</ol>
</box>
<box title="Compte-Rendu de la réunion du 04/06/04" link="040604">
Présents:<ul>
<li> Alain Frisch</li>
<li> Guillaume Gillard</li>
<li> Maurice Martin</li>
</ul>
<ol>
<li> Démonstration de l'atelier Brixlogic: scénario, itération,
sous-scénario, représentation graphique, représentation interne,
meta-data, chemin dans sample document.
</li>
<li> Explications sur la structure de l'implantation du système de type;
détails de représentation des combinaisons booléennes (arbres de décision
ternaire), formule de décomposition des produits sous forme d'arbre
binaire, implémentation du sous-typage avec cache et retour-arrière.
</li>
<li> Discussion: approche pour utiliser le sous-typage de CDuce dans
Brixlogic (solution probablement retenue: reimplémenter plutôt que de
réutiliser, pour maîtriser la technologie et optimiser en laissant tomber
les caractéristiques inutiles pour Brix); discussion sur le paradigme
graphique (Brix représente graphiquement le flot de controle; serait-il
souhaitable de représenter en plus/à la place le flot de données ?).
</li></ol>
</box>
<box title="Compte-Rendu de la réunion du 24/04/04" link="240404">
Présents:<ul>
<li> Alain Frisch</li>
<li> Véronique Benzaken</li>
<li> Giuseppe Castagna</li>
<li> Guillaume Gillard</li>
<li> Guillaume Lebleu</li>
<li> Maurice Martin</li>
<li> Cédric Miachon</li>
</ul>
<ol>
<li> Brixlogix : prototype visuel. 2 projets en cours. IFX et ACCORD. Probleme du <i>Change Impact Analysis</i>. utilisation des <i>WSDL</i>. typage incremental avec detection de typage instantane.
</li>
<li> CDuce : Ajout des standards (<i>namespaces</i> et <i>XML Schema</i>). Interface Ocaml/CDuce. Implatation de CDuce avec les motifs <i>jit</i>. Langage de requetes.
</li>
<li> Cooperation: Deleguer le typage a CDuce, ou ne reprendre que les algorithmes de typage, systeme de type?
</li>
</ol>
</box>
<box title="Présentation de GraphDuce" link="GDPres">
</box>
</page>
<?xml version="1.0" encoding="ISO-8859-1" standalone="yes"?>
<page name="graphduce">
<title>GraphDuce</title>
<left>
<boxes-toc/>
</left>
<include file="GD/cr040604.xml"/>
<box title="Presentation" link="main">
<p>
Le projet GraphDUCE est une collaboration entre le groupe de developpement de
CDuce et la societé <a href="http://www.brixlogic.com">Brixlogic</a>. Il a
pour objectif d'explorer la possibilité de mise en oeuvre d'un langage
dédié au traitement de documents XML qui ait les qualités suivantes:
</p>
<ol>
<li>interface utilisateur déclarative et/ou graphique, intuitive le rendant
accessible au plus grand nombre possible de développeurs dans le monde</li>
<li>vérification statique des types afin d'assurer un niveau de robustesse et
d'optimisation du code généré supérieur au meilleures technologies
actuellement disponibles sur le marché.</li>
<li>particulièrement
pertinent pour la mise en oeuvre de protocoles XML d'échanges de données
financières comme FIXML (Financial Information eXchange protocol), Visa 3D ou
encore IFX (Interactive Financial eXchange protocol).</li>
</ol>
<p>
La collaboration entre Brixlogic et CDuce s'articule autour de deux modes
d'utilisation différents de CDuce et offre une couverture du cycle de
production. En amont, Brixlogic effectue le traitement de l'information
XML. Ensuite le flux de cette information est géré dans le cadre plus
général de workflows d'entreprise. En chaque point du processus, CDuce est
utilisé à des fins distinctes
</p>
<p><b>XML et CDuce comme fin:</b> Brixlogic fournit un outil graphique pour la
manipulation de documents XML pour des standards financiers. XML est perçu
comme fin. Dans ce cadre, CDuce est utilisé comme langage final pour la
définition de toute (ou parties de) la transformation. Cet aspect de la
collaboration conduit à la production de code CDuce.
</p>
<p><b>XML et CDuce comme moyen:</b> Brixlogic fournit un outil graphique pour la
description en XML du workflow d'entreprise. Donc XML est perçu comme
outil. le but consiste à utiliser CDuce pour implanter un langage de
workflow.
</p>
<p><b>Apport pour CDuce:</b> Dans les deux cas, les avantages pour CDuce sont
multiples : (i) retour sur les caractéristiques du langage, (ii) accès au
savoir-faire en développement d'interfaces graphiques, (iii) bénéfice
du travail du développement d' outils "non-recherche", (iv) passage à
l'échelle: test en grandeur nature des possibilités du langage et de son
implantation.
</p>
<p><b>Apport pour Brixlogic:</b>
Concernant le premier aspect, l'avantage pour Brixlogic est triple : (i)
obtention de transformations certifiées 100% sûres, (ii) possibilité
d'ajouter des briques CDuces programmées par un programmeur spécialisé
en activité de conseil et (iii) augmentation de productivité.
<br/>
Relativement au deuxième aspect, l'avantage pour Brixlogic est double : (i)
utilisation d'un langage très adapté pour une telle modélisation :
higher order, typage, sûreté (ii) possibilité d'analyses statiques de
correction.
</p>
<section title="Verrous technologiques">
<ol>
<li> Définition d'une opération CDuce pour Brixlogic </li>
<li> Utilisation de programmes CDuce à l'intérieur de Brixlogic </li>
<li> Utilisation des techniques de typage de CDuce pour types les transformation
élémentaire de Brixlogic </li>
</ol>
</section>
<section title="Innovations et retombées économiques">
<p>
Le projet GraphDUCE se base sur l'association de Brixlogic, une société
spécialisée dans les outils graphiques pour la mise en oeuvre de
protocoles d'échange de données financières, et du groupe de recherche
CDuce (LIENS et LRI). La technologie résultant éventuellement de la
combinaison de ces expertises complémentaires pourra être transformée
en un produit unique en son genre, car alliant simplicité, robustesse et
performance, et qui pourra être commercialisée sur un marché mondial
représentant plusieurs centaines de millions voire plusieurs milliards
d'Euros
</p>
</section>
</box>
<box title="Documents" link="doc">
<p>Description scientifique du projet (<a href="descriptif_graphduce.pdf">PDF</a>)</p>
<p>Poster 2003 (<a href="poster-2003.pdf">PDF</a>)</p>
<p>Poster 2006 (<a href="poster-final.pdf">PDF</a>)</p>
</box>
<box title="Compte-Rendus" link="dcr">
<p><b><a href="CompteRendus.html#141004">Réunion du 14/10/04</a></b></p>
<p><b><a href="CompteRendus.html#040604">Réunion du 04/06/04</a></b></p>
<p><b><a href="CompteRendus.html#240404">Réunion du 24/04/04</a></b></p>
<p><b><a href="CompteRendus.html#GDPres">Présentation</a></b></p>
</box>
</page>
CDuce website: technical documentation
CDuce website is generated by "site.cd". The entry point is the file
"site.xml".
The site is structured as a tree of pages, with a single toplevel page
(normally "index").
Items on a page:
- box: a large box on the main panel
- meta: a special box on the main panel to display meta information
- left: a narrow box on the left panel
- page: a sub-page
- external: a "virtual" sub-page, not managed by site.cd but
integrated in the tree
Content:
- boxes-toc: list of links to all boxes on this page
- pages-toc: list of links to all subpages
- site-toc: global sitemap
- local-links: list of links to some arbitrary pages of the site
(href is a comma separted list of page names)
- footnote
- ...
USER MANUAL
===========
Add a table with complete syntax of type and patterns at the end of the
chapter on types and patterns.
Add syntactic sugar of references (pag 12)
DONE: Define exactly @ at page 10
Add section on Module system
TUTORIAL
========
- DONE PLEASE CHECK: update syntax for new elements
- explain syntax (x:? t) and why it is better for load xml in page 5
- finish the sections on patterns and references
- DONE: rewrite section on queries
ALL
===
DONE: (PDF) Add page numbers
DONE: (PDF) Add table of contents
<?xml version="1.0" encoding="ISO-8859-1" standalone="yes"?>
<page name="tralala">
<title>XML Transformation Languages: logic and applications (TraLaLA)</title>
<left>
<p style="font-size: 12pt; color: fuchsia">Available Pages</p>
<ul>
<li>Tralala</li>
<li><a href="tralala_partenaires.html">Partenaires</a> </li>
<li><a href="tralala_documents.html">Documents</a> </li>
<li><a href="tralala_reunions.html">Réunions</a> </li>
<li><a href="tralala_cr.html">Comptes rendus</a></li>
<li><a href="tralala_mailing.html">Listes de diffusion</a> </li>
</ul>
</left>
<include file="tralala_partenaires.xml"/>
<include file="tralala_documents.xml"/>
<include file="tralala_reunions.xml"/>
<include file="tralala_cr.xml"/>
<include file="tralala_mailing.xml"/>
<left>
Project funded by the
<a href="http://acimd.labri.fr/">ACI MASSES DE DONNÉES</a>
<p style="text-align: center"><img src="img/marianne.jpg" alt="Ministere de la recherche"/>
</p></left>
<left>
<p> All pages of this site were automatically generated from an XML description of
the content by <a href="examples.html#site">the following CDuce program</a>.
</p><p><img src="img/cducepower.jpg" alt="Powered by CDuce"/></p>
</left>
<box title="Description" link="des">
<p>
Notre projet se propose d'étudier les aspects de traitement,
d'interrogation et de manipulation de grandes masses de données lorsque
celles-ci sont disponibles au format XML. Nous nous intéressons plus
précisément aux aspects langages de programmation et langages de requêtes.
Notre ambition est de couvrir de manière intégrée un large spectre de
problématiques: de celles liées aux <b>aspects langages</b> (expressivité,
typage, étude de nouvelles primitives de programmation, logiques
sous-jacentes pour l'interrogation, optimisation logique), jusqu'aux aspects
traitant l'<b>accessibilité des données</b> (données en streaming,
compression, définition de modèles d'accès en mémoire secondaire, utilisation de moteurs de persistance), en passant par les
problématiques liées à <b>l'implantation</b> (compilation du filtrage,
optimisation physique, vérification du sous-typage, modèles d'exécution
pour le streaming).
</p>
<p>
Nous attaquerons ces problématiques en organisant notre recherche selon
trois axes directeurs: langages de requêtes, traitement de données à la
volée et typage de documents.
</p>
<ol style="list-style-type:none;">
<li><b>langages de requêtes</b> : étude théorique de paradigmes d'interrogation sous
l'angle de l'expressivité et de la complexité; définitions de langages de
requêtes pour XML ayant les caractéristiques d'expressivité restreinte et
de déclarativité typiques des langages du modèle relationnel ; implantation
puis conception et validation de techniques d'optimisations adaptées à ces
différents paradigmes.<br/><br/></li>
<li><b>traitement des données à la volée (streaming)</b> : identification d'une
classe de requêtes qu'il est possible d'évaluer par "streaming",
avec ou sans compression des données, et dans le premier cas de détermination de
la granularité optimale de compression.<br/><br/></li>
<li><b>contraintes et typage de documents</b> : vérification (efficace) de contraintes d'intégrités plus fines que
celles des langages traditionnels (par exemple, l'<i> interleaving</i> des éléments XML;
utilisation des types statiques pour
la compilation efficace et l'optimisation de requêtes).<br/>
</li></ol>
<p>
Outre une unité méthodologique, et une unité dans les objectifs, la
coopération au sein du projet est accrue par la décision de choisir
une cible logicielle unique à nos efforts d'implantation, le langage
CDuce, qui est développé conjointement par le LIENS et le LRI, deux
des sites participants à ce projet.
</p>
</box>
<box>
<img src="http://www.dilbert.com/comics/dilbert/archive/images/dilbert27330570070115.gif" alt="Dilbert" style="center"/>
</box>
</page>
<?xml version="1.0" encoding="ISO-8859-1" standalone="yes"?>
<page name="appli">
<title>Applications</title>
<left>
<local-links href="index,documentation"/>
</left>
<box>
<p>
This page collects some examples of applications that use CDuce.
</p>
<section title="CDuce to build web sites">
<ul>
<li>The <a href="http://www.cduce.org/">CDuce</a> site itself.</li>
<li><a href="http://www.random-art.org/">Random Art</a>.
(<a href="http://home.andrej.com/aikido/bin/">Source code</a>
for a similar site by the same author, Andrej Bauer.)</li>
<li><a href="http://www.larouedesecours.com/">La roue de
secours</a>.</li>
<li><a href="http://www.editionsvalroc.com/">ditions Valroc</a>.</li>
<li><a href="http://grip.ujf-grenoble.fr/index.html">Groupe de Rflexion Interdisciplinaire sur les Programmes</a>.</li>
</ul>
</section>
<section title="CDuce in scientific research projects">
<p>
Several research papers mention the use of CDuce.
</p>
<ul>
<li><a href="http://staff.science.uva.nl/~sfissaha/">Extracting
Temporal Information from Open Domain Text: A Comparative
Exploration</a>.</li>
<li><a href="http://www.irit.fr/recherches/TYPES/SVF/strecker/Publications/fesca05.html">Towards formalising AADL in Proof Assistants</a>.</li>
</ul>
</section>