Expressiveness of Concurrent Languages

The aim of this thesis is to go through different approaches for proving expressiveness properties in several concurrent languages. We analyse four different calculi exploiting for each one a different technique. We begin with the analysis of a synchronous language, we explore the expressiveness of a fragment of CCS! (a variant of Milner's CCS where replication is considered instead of recursion) w.r.t. the existence of faithful encodings (i.e. encodings that respect the behaviour of the encoded model without introducing unnecessary computations) of models of computability strictly less expressive than Turing Machines. Namely, grammars of types 1,2 and 3 in the Chomsky Hierarchy. We then move to asynchronous languages and we study full abstraction for two Linda-like languages. Linda can be considered as the asynchronous version of CCS plus a shared memory (a multiset of elements) that is used for storing messages. After having defined a denotational semantics based on traces, we obtain fully abstract semantics for both languages by using suitable abstractions in order to identify different traces which do not correspond to different behaviours. Since the ability of one of the two variants considered of recognising multiple occurrences of messages in the store (which accounts for an increase of expressiveness) reflects in a less complex abstraction, we then study other languages where multiplicity plays a fundamental role. We consider the language CHR (Constraint Handling Rules) a language which uses multi-headed (guarded) rules. We prove that multiple heads augment the expressive power of the language. Indeed we show that if we restrict to rules where the head contains at most n atoms we could generate a hierarchy of languages with increasing expressiveness (i.e. the CHR language allowing at most n atoms in the heads is more expressive than the language allowing at most m atoms, with mof the rewriting rules, several dialects of the calculus can be obtained. We analyse the expressive power of some of these dialects by focusing on decidability and undecidability for problems like reachability and coverability.

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

A core calculus for the analysis and implementation of biologically inspired languages

The application of Concurrency Theory to Systems Biology is in its earliest stage of progress. The metaphor of cells as computing systems by Regev and Shapiro opened the employment of concurrent languages for the modelling of biological systems. Their peculiar characteristics led to the design of many bio-inspired formalisms which achieve higher faithfulness and specificity. In this thesis we present pi@, an extremely simple and conservative extension of the pi-calculus representing a keystone in this respect, thanks to its expressiveness capabilities. The pi@ calculus is obtained by the addition of polyadic synchronisation and priority to the pi-calculus, in order to achieve compartment semantics and atomicity of complex operations respectively. In its direct application to biological modelling, the stochastic variant of the calculus, Spi@, is shown able to model consistently several phenomena such as formation of molecular complexes, hierarchical subdivision of the system into compartments, inter-compartment reactions, dynamic reorganisation of compartment structure consistent with volume variation. The pivotal role of pi@ is evidenced by its capability of encoding in a compositional way several bio-inspired formalisms, so that it represents the optimal core of a framework for the analysis and implementation of bio-inspired languages. In this respect, the encodings of BioAmbients, Brane Calculi and a variant of P Systems in pi@ are formalised. The conciseness of their translation in pi@ allows their indirect comparison by means of their encodings. Furthermore it provides a ready-to-run implementation of minimal effort whose correctness is granted by the correctness of the respective encoding functions. Further important results of general validity are stated on the expressive power of priority. Several impossibility results are described, which clearly state the superior expressiveness of prioritised languages and the problems arising in the attempt of providing their parallel implementation. To this aim, a new setting in distributed computing (the last man standing problem) is singled out and exploited to prove the impossibility of providing a purely parallel implementation of priority by means of point-to-point or broadcast communication.

Interpreting Judgements using Knowledge Representation Methods and Computational Models of Argument

The goal of the present research is to define a Semantic Web framework for precedent modelling, by using knowledge extracted from text, metadata, and rules, while maintaining a strong text-to-knowledge morphism between legal text and legal concepts, in order to fill the gap between legal document and its semantics. The framework is composed of four different models that make use of standard languages from the Semantic Web stack of technologies: a document metadata structure, modelling the main parts of a judgement, and creating a bridge between a text and its semantic annotations of legal concepts; a legal core ontology, modelling abstract legal concepts and institutions contained in a rule of law; a legal domain ontology, modelling the main legal concepts in a specific domain concerned by case-law; an argumentation system, modelling the structure of argumentation. The input to the framework includes metadata associated with judicial concepts, and an ontology library representing the structure of case-law. The research relies on the previous efforts of the community in the field of legal knowledge representation and rule interchange for applications in the legal domain, in order to apply the theory to a set of real legal documents, stressing the OWL axioms definitions as much as possible in order to enable them to provide a semantically powerful representation of the legal document and a solid ground for an argumentation system using a defeasible subset of predicate logics. It appears that some new features of OWL2 unlock useful reasoning features for legal knowledge, especially if combined with defeasible rules and argumentation schemes. The main task is thus to formalize legal concepts and argumentation patterns contained in a judgement, with the following requirement: to check, validate and reuse the discourse of a judge - and the argumentation he produces - as expressed by the judicial text.

A communication infrastructure to support knowledge level agents on the web

Agent Communication Languages (ACLs) have been developed to provide a way for agents to communicate with each other supporting cooperation in Multi-Agent Systems. In the past few years many ACLs have been proposed for Multi-Agent Systems, such as KQML and FIPA-ACL. The goal of these languages is to support high-level, human like communication among agents, exploiting Knowledge Level features rather than symbol level ones. Adopting these ACLs, and mainly the FIPA-ACL specifications, many agent platforms and prototypes have been developed. Despite these efforts, an important issue in the research on ACLs is still open and concerns how these languages should deal (at the Knowledge Level) with possible failures of agents. Indeed, the notion of Knowledge Level cannot be straightforwardly extended to a distributed framework such as MASs, because problems concerning communication and concurrency may arise when several Knowledge Level agents interact (for example deadlock or starvation). The main contribution of this Thesis is the design and the implementation of NOWHERE, a platform to support Knowledge Level Agents on the Web. NOWHERE exploits an advanced Agent Communication Language, FT-ACL, which provides high-level fault-tolerant communication primitives and satisfies a set of well defined Knowledge Level programming requirements. NOWHERE is well integrated with current technologies, for example providing full integration for Web services. Supporting different middleware used to send messages, it can be adapted to various scenarios. In this Thesis we present the design and the implementation of the architecture, together with a discussion of the most interesting details and a comparison with other emerging agent platforms. We also present several case studies where we discuss the benefits of programming agents using the NOWHERE architecture, comparing the results with other solutions. Finally, the complete source code of the basic examples can be found in appendix.

Constraint handling rules. Compositional semantics and program transformation

This thesis intends to investigate two aspects of Constraint Handling Rules (CHR). It proposes a compositional semantics and a technique for program transformation. CHR is a concurrent committed-choice constraint logic programming language consisting of guarded rules, which transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion [Frü06] and it belongs to the declarative languages family. It was initially designed for writing constraint solvers but it has recently also proven to be a general purpose language, being as it is Turing equivalent [SSD05a]. Compositionality is the first CHR aspect to be considered. A trace based compositional semantics for CHR was previously defined in [DGM05]. The reference operational semantics for such a compositional model was the original operational semantics for CHR which, due to the propagation rule, admits trivial non-termination. In this thesis we extend the work of [DGM05] by introducing a more refined trace based compositional semantics which also includes the history. The use of history is a well-known technique in CHR which permits us to trace the application of propagation rules and consequently it permits trivial non-termination avoidance [Abd97, DSGdlBH04]. Naturally, the reference operational semantics, of our new compositional one, uses history to avoid trivial non-termination too. Program transformation is the second CHR aspect to be considered, with particular regard to the unfolding technique. Said technique is an appealing approach which allows us to optimize a given program and in more detail to improve run-time efficiency or spaceconsumption. Essentially it consists of a sequence of syntactic program manipulations which preserve a kind of semantic equivalence called qualified answer [Frü98], between the original program and the transformed ones. The unfolding technique is one of the basic operations which is used by most program transformation systems. It consists in the replacement of a procedure-call by its definition. In CHR every conjunction of constraints can be considered as a procedure-call, every CHR rule can be considered as a procedure and the body of said rule represents the definition of the call. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. We define an unfolding rule, show its correctness and discuss some conditions in which it can be used to delete an unfolded rule while preserving the meaning of the original program. Finally, confluence and termination maintenance between the original and transformed programs are shown. This thesis is organized in the following manner. Chapter 1 gives some general notion about CHR. Section 1.1 outlines the history of programming languages with particular attention to CHR and related languages. Then, Section 1.2 introduces CHR using examples. Section 1.3 gives some preliminaries which will be used during the thesis. Subsequentely, Section 1.4 introduces the syntax and the operational and declarative semantics for the first CHR language proposed. Finally, the methodologies to solve the problem of trivial non-termination related to propagation rules are discussed in Section 1.5. Chapter 2 introduces a compositional semantics for CHR where the propagation rules are considered. In particular, Section 2.1 contains the definition of the semantics. Hence, Section 2.2 presents the compositionality results. Afterwards Section 2.3 expounds upon the correctness results. Chapter 3 presents a particular program transformation known as unfolding. This transformation needs a particular syntax called annotated which is introduced in Section 3.1 and its related modified operational semantics !0t is presented in Section 3.2. Subsequently, Section 3.3 defines the unfolding rule and prove its correctness. Then, in Section 3.4 the problems related to the replacement of a rule by its unfolded version are discussed and this in turn gives a correctness condition which holds for a specific class of rules. Section 3.5 proves that confluence and termination are preserved by the program modifications introduced. Finally, Chapter 4 concludes by discussing related works and directions for future work.

Costrutti ed Applicazioni di Programmazione Generica in Linguaggi Object-Oriented

Generic programming is likely to become a new challenge for a critical mass of developers. Therefore, it is crucial to refine the support for generic programming in mainstream Object-Oriented languages — both at the design and at the implementation level — as well as to suggest novel ways to exploit the additional degree of expressiveness made available by genericity. This study is meant to provide a contribution towards bringing Java genericity to a more mature stage with respect to mainstream programming practice, by increasing the effectiveness of its implementation, and by revealing its full expressive power in real world scenario. With respect to the current research setting, the main contribution of the thesis is twofold. First, we propose a revised implementation for Java generics that greatly increases the expressiveness of the Java platform by adding reification support for generic types. Secondly, we show how Java genericity can be leveraged in a real world case-study in the context of the multi-paradigm language integration. Several approaches have been proposed in order to overcome the lack of reification of generic types in the Java programming language. Existing approaches tackle the problem of reification of generic types by defining new translation techniques which would allow for a runtime representation of generics and wildcards. Unfortunately most approaches suffer from several problems: heterogeneous translations are known to be problematic when considering reification of generic methods and wildcards. On the other hand, more sophisticated techniques requiring changes in the Java runtime, supports reified generics through a true language extension (where clauses) so that backward compatibility is compromised. In this thesis we develop a sophisticated type-passing technique for addressing the problem of reification of generic types in the Java programming language; this approach — first pioneered by the so called EGO translator — is here turned into a full-blown solution which reifies generic types inside the Java Virtual Machine (JVM) itself, thus overcoming both performance penalties and compatibility issues of the original EGO translator. Java-Prolog integration Integrating Object-Oriented and declarative programming has been the subject of several researches and corresponding technologies. Such proposals come in two flavours, either attempting at joining the two paradigms, or simply providing an interface library for accessing Prolog declarative features from a mainstream Object-Oriented languages such as Java. Both solutions have however drawbacks: in the case of hybrid languages featuring both Object-Oriented and logic traits, such resulting language is typically too complex, thus making mainstream application development an harder task; in the case of library-based integration approaches there is no true language integration, and some “boilerplate code” has to be implemented to fix the paradigm mismatch. In this thesis we develop a framework called PatJ which promotes seamless exploitation of Prolog programming in Java. A sophisticated usage of generics/wildcards allows to define a precise mapping between Object-Oriented and declarative features. PatJ defines a hierarchy of classes where the bidirectional semantics of Prolog terms is modelled directly at the level of the Java generic type-system.

Security control brought back to the user

The activity of the Ph.D. student Juri Luca De Coi involved the research field of policy languages and can be divided in three parts. The first part of the Ph.D. work investigated the state of the art in policy languages, ending up with: (i) identifying the requirements up-to-date policy languages have to fulfill; (ii) defining a policy language able to fulfill such requirements (namely, the Protune policy language); and (iii) implementing an infrastructure able to enforce policies expressed in the Protune policy language. The second part of the Ph.D. work focused on simplifying the activity of defining policies and ended up with: (i) identifying a subset of the controlled natural language ACE to express Protune policies; (ii) implementing a mapping between ACE policies and Protune policies; and (iii) adapting the ACE Editor to guide users step by step when defining ACE policies. The third part of the Ph.D. work tested the feasibility of the chosen approach by applying it to meaningful real-world problems, among which: (i) development of a security layer on top of RDF stores; and (ii) efficient policy-aware access to metadata stores. The research activity has been performed in tight collaboration with the Leibniz Universität Hannover and further European partners within the projects REWERSE, TENCompetence and OKKAM.

Il dialogo con l'infanzia. Utopia del folklore, nonsense e comico in Gianni Rodari.

Nel trentennale dalla morte di Gianni Rodari, la tesi elabora problemi e riflessioni circa la maggiore urgenza corrente tra gli attuali studi rodariani: la necessità, per la cultura nazionale, di conferire a Gianni Rodari e alla letteratura per l’infanzia il ruolo intellettuale determinante da essi rivestito. La tesi sceglie di concentrarsi sui maggiori libri poetici e sul capolavoro teorico, la Grammatica della fantasia, utilizzando come strumenti il confronto con Gramsci, con la tradizione del folklore, con i grandi scrittori per l’infanzia dell’Inghilterra e con le altre esperienze poetiche del Novecento, discutendo Rodari da una specola esclusivamente filologica e letteraria. Parte prima: Rodari utopista. Nella prima parte Gianni Rodari viene inquadrato in un confronto diretto con l’Antonio Gramsci dei Quaderni, che aveva lucidamente individuato la separatezza tutta italiana tra classe intellettuale e mondo popolare, con conseguente inesistenza di una letteratura nazionale-popolare e di una specifica letteratura per l’infanzia. Rodari, primo intellettuale a dedicare tutto se stesso al riempimento di questa lacuna, risponde con intento sociale e politico al problema, adottando un atteggiamento che la tesi definisce utopico. Tramite una disamina del pensiero delle utopie letterarie a confronto con la tradizione popolare del paese di Cuccagna, la tesi procede all’accurato rinvenimento nell’opera di Rodari dei luoghi utopici, tutti orientati a suggerire un utilizzo dell’utopia come chiave per forzare un presente insoddisfacente e accedere a un futuro costruito da ogni individuo in prima persona. Parte seconda: Rodari poeta nonsense? Scritta in Inghilterra presso l’Istitute of Germanic and Romance Studies della University of London, la seconda e corposa parte della tesi si propone come un ampliamento della traccia gettata nel 1983 dall’articolo di Cristina Bertea Gianni Rodari in Gran Bretagna. La tesi analizza dapprima il problema del nonsense, ancora scarsamente trattato in Italia, riflettendo criticamente sulla maggiore bibliografia anglosassone che ha studiato il tema. Successivamente, mette a raffronto il lavoro linguistico che Gianni Rodari ha compiuto lungo l’arco di tutta la vita e le tecniche di composizione poetica elaborate nella Grammatica della fantasia con gli strumenti retorico-formali del nonsense individuati nell’opera di Lewis Carroll, di Edward Lear e delle nursery rhymes inglesi. Parte terza: Traccia per una mappatura della poesia per l’infanzia in Italia, a partire da Gianni Rodari. L’ultima parte della tesi si avventura alla ricerca di un percorso possibile attraverso la poesia per l’infanzia del Novecento e le sue esperienze di comicità. I capitoli si soffermano sul nonsense di Toti Scialoja e di Nico Orengo, sui precedenti di Lina Schwarz e Alfonso Gatto, sul Petel di Zanzotto, sulla poesia di soglia di Vivian Lamarque e sull’eredità della Grammatica della fantasia con particolare riferimento a Calicanto, di Ersilia Zamponi e Roberto Piumini.

Constraints meet concurrency

We investigate the benefits that emerge when the fields of constraint programming and concurrency meet. On one hand, constraints can be use in concurrency theory to increase the conciseness and the expressive power of concurrent languages from a pragmatic point of view. On the other hand, problems modeled by using constraints can be solved faster and more efficiently using a concurrent system. We explore both directions providing two separate lines of contribution. Firstly we study the expressive power of a concurrent language, namely Constraint Handling Rules, that supports constraints as a primitive construct. We show what features of this language make it Turing powerful. Then we propose a framework to solve constraint problems that is intended to be deployed on a concurrent system. For the development of this framework we used the concurrent language Jolie following the Service Oriented paradigm. Based on this experience, we also propose an extension to Service Oriented Languages to overcome some of their limitations and to improve the development of concurrent applications.

Contaminazioni tra arte e architettura

Il concetto di contaminazione fra architettura ed arti plastiche e figurative è molto antico. La dicotomia arte-architettura, sancita in via definitiva con il moderno museo di spoliazione napoleonica, non può che essere considerata una variazione neo-tecnicista sulla quale, non sempre giustamente, sono andati assestandosi gli insegnamenti delle scuole politecniche. Non così è sempre stato. Come il tempio greco può essere considerato un’opera plastica nel suo complesso, esempio tra i primi di fusione tra arte e architettura, moltissimi sono gli esempi che hanno guidato la direzione della ricerca che si è intesa perseguire. Molti sono gli esempi del passato che ci presentano figure di architetto-artista: un esempio fra tutti Michelangelo Buonarroti; come per altro non è nuovo, per l’artista puro, cimentarsi nella progettazione dello spazio architettonico o urbano, o per l'architetto essere coinvolto dalle indagini della ricerca artistica a lui contemporanea dalla quale trarre suggestioni culturali. Le rappresentazioni dei linguaggi visivi sono il frutto di contaminazioni che avvengono su diversi livelli e in più direzioni. Spesso le ricerche artistiche più significative hanno anticipato o influenzato il mondo del design, dell’architettura, della comunicazione. L’intenzione della ricerca è stata quindi approfondire, attraverso un viaggio nel Novecento, con particolare attenzione al Secondo Dopoguerra, i fenomeni culturali che hanno prodotto i più significativi sviluppi stilistici nell’ambito della ricerca e del rinnovo del linguaggio architettonico. Il compito, parafrasando Leonardo Benevolo, non è stato quello di elencare le singole battute della discussione ma di riconoscere gli interventi fruttuosi a lunga scadenza. Mutuando gli insegnamenti della scuola del Bauhaus, arte e architettura sono state affiancate perché considerate espressioni strettamente relazionate di coevi fenomeni culturali. L’obiettivo ha puntato all’individuazione dei meccanismi delle interazioni tra discipline, cercando di delineare il profilo della complessità dell’espressione del contemporaneo in architettura.

L'Architettura religiosa di Luis Moya Blanco. La costruzione come principio compositivo

La presente ricerca, L’architettura religiosa di Luis Moya Blanco. La costruzione come principio compositivo, tratta i temi inerenti l’edificazione di spazi per il culto della religione cristiana che l’architetto spagnolo progetta e realizza a Madrid dal 1945 al 1970. La tesi è volta ad indagare quali siano i principi alla base della composizione architettonica che si possano considerare immutati, nel lungo arco temporale in cui l’autore si trova ad operare. Tale indagine, partendo da una prima analisi riguardante gli anni della formazione e gli scritti da lui prodotti, verte in particolare sullo studio dei progetti più recenti e ancora poco trattati dalla critica. L’obbiettivo della presente tesi è dunque quello di apportare un contributo originale sull’aspetto compositivo della sua architettura. Ma analizzare la composizione significa, in Moya, analizzare la costruzione che, a dispetto del susseguirsi dei linguaggi, rimarrà l’aspetto principale delle sue opere. Lo studio dei manufatti mediante categorie estrapolate dai suoi stessi scritti – la matematica, il numero, la geometria e i tracciati regolatori - permette di evidenziare punti di contatto e di continuità tra le prime chiese, fortemente caratterizzate da un impianto barocco, e gli ultimi progetti che sembrano cercare invece un confronto con forme decisamente moderne. Queste riflessioni, parallelamente contestualizzate nell’ambito della sua consistente produzione saggistica, andranno a confluire nell’idea finale per cui la costruzione diventi per Luis Moya Blanco il principio compositivo da cui non si può prescindere, la regola che sostanzia nella materia il numero e la geometria. Se la costruzione è dunque la pietrificazione di leggi geometrico-matematiche che sottendono schemi planimetrici; il ricorso allo spazio di origine centrale non risponde all’intenzione di migliorare la liturgia, ma a questioni di tipo filosofico-idealista, che fanno corrispondere alla somma naturalezza della perfezione divina, la somma perfezione della forma circolare o di uno dei suoi derivati come l’ellisse.

Il linguaggio figurato e la cabina di simultanea: Il progetto IMITES(Interpretación de la Metáfora entre ITaliano y ESpañol)

Il progetto di dottorato IMITES (Interpretación de la Metáfora entre ITaliano y ESpañol) si pone come obiettivo quello di analizzare l’interpretazione simultanea del linguaggio figurato nelle combinazioni italiano-spagnolo e spagnolo-italiano. Prevede l’analisi di una serie di dati estratti da discorsi pronunciati in italiano e spagnolo in occasione di conferenze tenutesi presso la Commissione europea, e le loro versioni interpretate in spagnolo e italiano rispettivamente. Le espressioni figurate contenute nei discorsi originali sono state allineate e messe a confronto con le versioni fornite dagli interpreti, con il duplice obiettivo di a) capire quali causano maggiori problemi agli interpreti e b) analizzare le strategie di interpretazione applicate da professionisti quali quelli della Direzione Generale Interpretazione (DG SCIC) della Commissione europea nell’interpretare metafore. Il progetto prevede anche la somministrazione di un questionario agli interpreti delle cabine spagnola e italiana del DG SCIC, con l’obiettivo di sondare la loro percezione delle difficoltà che sottendono all’interpretazione del linguaggio figurato, le indicazioni metodologiche ricevute (se del caso) dai loro docenti a tale riguardo e le strategie applicate nella pratica professionale. Infine, l’ultima fase del progetto di ricerca prevede la sperimentazione di una proposta didattica attraverso uno studio caso-controllo svolto su studenti del secondo anno della Laurea Magistrale in Interpretazione delle Scuole Interpreti di Forlì e Trieste. Il gruppo-caso ha ricevuto una formazione specifica sull'interpretazione delle metafore, mentre gruppo-controllo è stato monitorato nella sua evoluzione. L’obiettivo di questa ultima fase di ricerca è quello di valutare, da una parte, l’ “insegnabilità” di strategia per affrontare il linguaggio figurato in interpretazione simultanea, e, dall’altra, l’efficacia dell’unità didattica proposta, sviluppata in base all’analisi svolta su IMITES.

Structural patterns for document engineering: from an empirical bottom-up analysis to an ontological theory

This thesis aims at investigating a new approach to document analysis based on the idea of structural patterns in XML vocabularies. My work is founded on the belief that authors do naturally converge to a reasonable use of markup languages and that extreme, yet valid instances are rare and limited. Actual documents, therefore, may be used to derive classes of elements (patterns) persisting across documents and distilling the conceptualization of the documents and their components, and may give ground for automatic tools and services that rely on no background information (such as schemas) at all. The central part of my work consists in introducing from the ground up a formal theory of eight structural patterns (with three sub-patterns) that are able to express the logical organization of any XML document, and verifying their identifiability in a number of different vocabularies. This model is characterized by and validated against three main dimensions: terseness (i.e. the ability to represent the structure of a document with a small number of objects and composition rules), coverage (i.e. the ability to capture any possible situation in any document) and expressiveness (i.e. the ability to make explicit the semantics of structures, relations and dependencies). An algorithm for the automatic recognition of structural patterns is then presented, together with an evaluation of the results of a test performed on a set of more than 1100 documents from eight very different vocabularies. This language-independent analysis confirms the ability of patterns to capture and summarize the guidelines used by the authors in their everyday practice. Finally, I present some systems that work directly on the pattern-based representation of documents. The ability of these tools to cover very different situations and contexts confirms the effectiveness of the model.