O canteiro do poeta-arquiteto: a conduta criativa de João Cabral de Melo Neto à luz de seus manuscritos

Neste artigo repensamos a metáfora do "poeta-engenheiro", ou "poeta-arquiteto", que geralmente caracteriza o processo criativo de João Cabral de Melo Neto, à luz de uma leitura genética de manuscritos de A educação pela pedra. Veremos que o "arquiteto" da metáfora provém da teoria de Le Corbusier, na qual o desenho (a concepção) determina o canteiro (a execução). No entanto, a análise de transformações de estruturas por meio de reformulações textuais nos manuscritos do poeta mostra que, por vezes, o projeto, ou intenção, se transforma nos trabalhos da página-canteiro.

O envolvimento da atenção na codificação da informação visuoespacial integrada

O objetivo deste estudo foi investigar o envolvimento de recursos da atenção na codificação e manutenção da informação visual e espacial na memória de trabalho. Utilizou-se um paradigma de tarefas duplas em que uma tarefa primária de localização espacial foi realizada simultaneamente a uma tarefa atentiva secundária de discriminação de tons. O desempenho dos participantes (n = 20) na tarefa primária foi afetado pela presença e pela similaridade entre os tons da tarefa secundária, e também, pela instrução de priorizar uma ou outra tarefa. Os resultados indicam que recursos atentivos (do executivo central) estão envolvidos na codificação e na manutenção ativa da informação integrada na memória visuoespacial, assim como na manutenção dos objetivos das tarefas a serem realizadas simultaneamente.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Expressiveness in biologically inspired languages

A very recent and exciting new area of research is the application of Concurrency Theory tools to formalize and analyze biological systems and one of the most promising approach comes from the process algebras (process calculi). A process calculus is a formal language that allows to describe concurrent systems and comes with well-established techniques for quantitative and qualitative analysis. Biological systems can be regarded as concurrent systems and therefore modeled by means of process calculi. In this thesis we focus on the process calculi approach to the modeling of biological systems and investigate, mostly from a theoretical point of view, several promising bio-inspired formalisms: Brane Calculi and k-calculus family. We provide several expressiveness results mostly by means of comparisons between calculi. We provide a lower bound to the computational power of the non Turing complete MDB Brane Calculi by showing an encoding of a simple P-System into MDB. We address the issue of local implementation within the k-calculus family: whether n-way rewrites can be simulated by binary interactions only. A solution introducing divergence is provided and we prove a deterministic solution preserving the termination property is not possible. We use the symmetric leader election problem to test synchronization capabilities within the k-calculus family. Several fragments of the original k-calculus are considered and we prove an impossibility result about encoding n-way synchronization into (n-1)-way synchronization. A similar impossibility result is obtained in a pure computer science context. We introduce CCSn, an extension of CCS with multiple input prefixes and show, using the dining philosophers problem, that there is no reasonable encoding of CCS(n+1) into CCSn.

Fonti cartografiche di Toscana e Catalogna di Età Moderna e Contemporanea. Ricostruire con il GIS, comunicare con WebGIS

The aim of this study is the creation of a Historical GIS that spatially reference data retrieved from Italian and Catalan historical sources and records. The generation of locates these metasource was achieved through the integral acquisition of source-oriented records and the insertion of mark-up fields, yet maintaining, where possible, the original encoding of the source documents. In order to standardize the set of information contained in the original documents and thus allow queries to the database, additional fields were introduced. Once the initial phase of data research and analysis was concluded the new virtual source was published online within an open WebGIS source. As a conclusion we have created a dynamic and spatially referenced database of geo-historical information. The configuration of this new source is such to guarantee the best possible accessibility.

L'area dei Lungarni di Pisa nel tardo Medioevo (XIV-XV secolo). un tentativo di ricostruzione in 3D.

Lo scopo di questa ricerca è la ricostruzione dei Lungarni di Pisa nel Tardo Medioevo (XIV-XV secolo); lo studio intende sottolineare le trasformazioni urbanistiche che hanno cambiato il volto di Pisa nel corso del tempo e ricordare che l’area fluviale ebbe un ruolo di primo piano come baricentro commerciale ed economico della città, vocazione che si è in gran parte persa con l’età moderna e contemporanea. La metodologia seguita, affinata e perfezionata durante la partecipazione al progetto Nu.M.E. (Nuovo Museo Elettronico della Città di Bologna), si basa sull’analisi e il confronto di fonti eterogenee ma complementari, che includono precedenti studi di storia dell’urbanistica, un corpus di documentazione di epoca medievale (provvedimenti amministrativi come gli Statuti del Comune di Pisa, ma anche descrizioni di cronisti e viaggiatori), fonti iconografiche, tra cui vedute e mappe cinquecentesche o successive, e fonti materiali, come le persistenze medievali ancora osservabili all’interno degli edifici ed i reperti rinvenuti durante alcune campagne di scavo archeologiche. Il modello 3D non è concepito come statico e “chiuso”, ma è liberamente esplorabile all’interno di un engine tridimensionale; tale prodotto può essere destinato a livelli di utenza diversi, che includono sia studiosi e specialisti interessati a conoscere un maggior numero di informazioni e ad approfondire la ricerca, sia semplici cittadini appassionati di storia o utenti più giovani, come studenti di scuole medie superiori e inferiori.

Il Montalbano nel Medioevo: Strumenti informatici per l’analisi archeologica del territorio e delle strutture architettoniche

La ricerca ha preso in esame l’analisi archeologica di un territorio medievale e la sperimentazione di strumenti informatici per la gestione e l’analisi dei dati prodotti dalla ricerca stessa. Il Montalbano, oggetto della ricerca, è una microregione caratterizzata da elementi che la rendono molto interessante. Si tratta di una catena submontana che divide la piana di Firenze-Prato-Pistoia dal Valdarno inferiore. Questa posizione di frontiera ne ha fatto l’oggetto di mire espansionistiche da parte delle principali famiglie signorili prima, dei comuni poi. In una prima fase sono stati censiti i siti attestati dalle fonti documentarie e materiali per capire le dinamiche insediative del popolamento medievale e le strategie di controllo di un territorio caratterizzato dall’assenza di un’egemonia da parte di un solo potere (almeno fino a metà ‘300). L’analisi stratigrafica si è poi concentrata sulle strutture architettoniche religiose, in quanto offrono la maggior quantità di dati dal punto di vista documentario e archeologico. È stato così possibile ottenere un quadro delle tecniche costruttive medievali e delle influenze culturali che lo hanno prodotto. I dati archeologici sono stati gestiti attraverso una piattaforma gis sviluppata all’interno del Laboratorio di Archeologia Medievale dell’Università di Firenze in collaborazione con il laboratorio LSIS del CNRS di Marsiglia. Questa è stata appositamente strutturata secondo le procedure di raccolta e organizzazione dati utilizzate durante l’analisi archeologica. Le singole strutture indagate sono inoltre state oggetto di un rilievo 3d fotogrammetrico che in alcuni casi studio è stato anche utilizzato come base di accesso ai dati derivanti dall’analisi stratigrafica, all’interno di un’applicazione gis 3d (Arpenteur). Questo ha permesso di connettere all’interno di un’unica piattaforma i dati geometrici ed archeometrici con quelli archeologici, utilizzando i primi come interfaccia di accesso ai secondi.

La costruzione della città medievale. Archeologia dell'edilizia storica e topografia urbana a Pistoia.

Pistoia rientra a buon diritto, nel quadro della Toscana medievale, in quella rete di centri urbani di antica origine e tradizione diocesana che riuscirono a costruire, nella dialettica fra città e territorio, un organismo politico autonomo, il comune cittadino. La ricerca prende in considerazione i resti materiali delle strutture conservate nel tessuto urbano attuale, in particolare l'edilizia civile, prediligendo la cosiddetta “edilizia minore”, ovvero gli edifici residenziali non monumentali che, proprio per questo motivo, sono generalmente poco conosciuti. Le strutture, censite ed inserite in una piattaforma GIS (Arpenteur), sono analizzate con metodo archeologico al fine di distinguere le diverse fasi costruttive, medievali e post-medievali, con cui sono giunte fino ad oggi. L'analisi stratigrafica, effettuata su rilievi realizzati mediante modellazione 3D (Photomodeler), ha permesso di costruire un primo “atlante” delle tipologie murarie medievali della città: i tipi murari assumono quindi la funzione di indicatori cronologici degli edifici analizzati. I dati stratigrafici, uniti al dato topologico dei complessi architettonici (localizzati prevalentemente nel centro storico, all'interno del circuito murario della metà del XII secolo), hanno fornito informazioni sia per quanto riguarda l'aspetto materiale degli edifici di abitazione (forma, dimensioni, materiali) sia per quanto riguarda temi di topografia storica (viabilità maggiore e minore, formazione dei borghi, orizzonte sociale degli abitanti, distribuzione della proprietà), nel periodo della “parabola” della Pistoia comunale (XII-XIII secolo). In conclusione, la ricerca vuole essere sia uno strumento di analisi per la storia delle trasformazioni delle città nel periodo comunale, sia uno strumento di conoscenza e tutela di un patrimonio storico-archeologico che, per la sua natura non-monumentale spesso sfugge all'attenzione di amministratori ed urbanisti.

Mangia, bevi, ama. Cibo e rituali alimentari del matrimonio nell'Occidente altomedievale

La ricerca pone al centro dell’indagine lo studio dell’importanza del cibo nelle cerimonie nuziali dell’Europa occidentale nei secoli V-XI. Il corpus di fonti utilizzate comprende testi di genere diverso: cronache, annali, agiografie, testi legislativi, a cui si è aggiunta un’approfondita analisi delle antiche saghe islandesi. Dopo un'introduzione dedicata in particolare alla questione della pubblicità della celebrazione, la ricerca si muove verso lo studio del matrimonio come “processo” sulla base della ritualità alimentare: i brindisi e i banchetti con cui si sigla l’accordo di fidanzamento e i ripetuti convivi allestiti per celebrare le nozze. Si pone attenzione anche ad alcuni aspetti trasversali, come lo studio del caso della “letteratura del fidanzamento bevuto”, ossia una tradizione di testi letterari in cui il fidanzamento tra i protagonisti viene sempre ratificato con un brindisi; a questo si aggiunge un’analisi di stampo antropologico della "cultura dell’eccesso", tipica dei rituali alimentari nuziali nel Medioevo, in contrasto con la contemporanea "cultura del risparmio". L'analisi si concentra anche sulle reiterate proibizioni al clero, da parte della Chiesa, di partecipare a banchetti e feste nuziali, tratto comune di tutta l’epoca altomedievale. Infine, la parte conclusiva della ricerca è incentrata sulla ricezione altomedievale di due figure bibliche che pongono al centro della narrazione un banchetto nuziale: la parabola delle nozze e il banchetto di Cana. L’insistente presenza di questi due brani nelle parole dei commentatori biblici mostra la straordinaria efficacia del “linguaggio alimentare”, ossia di un codice linguistico basato sul cibo (e su contesti quali l’agricoltura, la pesca, ecc.) come strumento di comunicazione sociale di massa con una valenza antropologica essenzialmente universale.

Type Systems for Distributed Programs: Components and Sessions

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.

Il codice autografo di Piero Giustinian: Un esempio di genesi ed evoluzione della cronachistica medievale

La tesi di dottorato di Luca Fiori: Il codice autografo di Piero Giustinian: un esempio di genesi ed evoluzione della cronachistica medievale ha il principale obiettivo quello di dimostrare attraverso la editio princeps dell’autografo in latino, i meccanismi di formazione, trasmissione e proliferazione dei testi cronachistici medievali veneziani, mediante la collazione disamina della tradizione testuale di Pietro Giustinian.

The posterior parietal cortex: a bridge between vision and action

The present work takes into account three posterior parietal areas, V6, V6A, and PEc, all operating on different subsets of signals (visual, somatic, motor). The work focuses on the study of their functional properties, to better understand their respective contribution in the neuronal circuits that make possible the interactions between subject and external environment. In the caudalmost pole of parietal lobe there is area V6. Functional data suggest that this area is related to the encoding of both objects motion and ego-motion. However, the sensitivity of V6 neurons to optic flow stimulations has been tested only in human fMRI experiments. Here we addressed this issue by applying on monkey the same experimental protocol used in human studies. The visual stimulation obtained with the Flow Fields stimulus was the most effective and powerful to activate area V6 in monkey, further strengthening this homology between the two primates. The neighboring areas, V6A and PEc, show different cytoarchitecture and connectivity profiles, but are both involved in the control of reaches. We studied the sensory responses present in these areas, and directly compared these.. We also studied the motor related discharges of PEc neurons during reaching movements in 3D space comparing also the direction and depth tuning of PEc cells with those of V6A. The results show that area PEc and V6A share several functional properties. Area PEc, unlike V6A, contains a richer and more complex somatosensory input, and a poorer, although complex visual one. Differences emerged also comparing the motor-related properties for reaches in depth: the incidence of depth modulations in PEc and the temporal pattern of modulation for depth and direction allow to delineate a trend among the two parietal visuomotor areas.

Deficit in the Emotional Embodiment in Alexithymia

Alexithymia refers to difficulties in recognizing one’s own emotions and others emotions. Theories of emotional embodiment suggest that, in order to understand other peoples’ feelings, observers re-experience, or simulate, the relevant component (i.e. somatic, motor, visceral) of emotion’s expressed by others in one’s self. In this way, the emotions are “embodied”. Critically, to date, there are no studies investigating the ability of alexithymic individuals in embodying the emotions conveyed by faces. In the present dissertation different implicit paradigms and techniques falling within the field of affective neuroscience have been employed in order to test a possible deficit in the embodiment of emotions in alexithymia while subjects were requested to observe faces manifesting different expression: fear, disgust, happiness and neutral. The level of the perceptual encoding of emotional faces and the embodiment of emotions in the somato-sensory and sensory-motor system have been investigated. Moreover, non-communicative motor reaction to emotional stimuli (i.e. visceral reactions) and interoceptive abilities of alexithymic subjects have been explored. The present dissertation provided convergent evidences in support of a deficit in the processing of fearful expression in subjects with high alexithymic personality traits. Indeed, the pattern of fear induced changes in the perceptual encoding, in the somato-sensory and in the somato-motor system (both the communicative and non communicative one) is widely and consistently altered in alexithymia. This support the hypothesis of a diminished responses to fearful stimuli in alexithymia. In addition, the overall results on happiness and disgust, although preliminary, provided interesting results. Indeed, the results on happiness revealed a defective perceptual encoding, coupled with a slight difficulty (i.e. delayed responses) at the level of the communicative somato-motor system, and the emotion of disgust has been found to be abnormally embodied at the level of the somato-sensory system.

Negativi di memoria. La rappresentazione del trauma nel romanzo del Novecento. Samuel Beckett, Georges Perec, Agota Kristof

Oggetto di questa tesi è l’analisi delle modalità di rappresentazione del trauma nel romanzo del Novecento e, in particolare, nelle opere di Samuel Beckett, Georges Perec e Agota Kristof. Fondamento dello studio sarà una disamina dei procedimenti linguistici e narrativi di rappresentazione del trauma nelle prose degli autori citati, al fine tracciare le linee di un’estetica in grado di descrivere le caratteristiche peculiari delle narrazioni in cui la dimensione antinarrativa della memoria traumatica assume il ruolo di principio estetico guida. L’analisi si soffermerà sulla cruciale relazione esistente, in tutti e tre gli autori, tra rappresentazione del trauma e sviluppo di strategie narrativi definibili come “denegative”. L’analisi dei testi letterari è condotta sulla base del corpus critico dei Trauma Studies, dell’ermeneutica della narrazione di stampo ricœuriano e della teoria del linguaggio psicoanalitica e affiancata, ove possibile, da uno studio filologico-genetico dei materiali d’autore. Alla luce di tali premesse, intendo rivalutare il carattere rappresentativo e testimoniale della letteratura del secolo scorso, in contrasto con la consuetudine a vedere nel romanzo novecentesco il trionfo dell’antimimesi e il declino del racconto. Dal momento che le narrazioni traumatiche si costruiscono intorno e attraverso i vuoti di linguaggio, la tesi è che siano proprio questi vuoti linguistici e narrativi (amnesie, acronie, afasie, lapsus, omissioni e mancanze ancora più sofisticate come nel caso di Perec) a rappresentare, in modo mimetico, la realtà apparentemente inaccessibile del trauma. Si tenterà di dimostrare come questi nuovi canoni di rappresentazione non denuncino l’impossibilità del racconto, bensì una sfida al silenzio, celata in più sottili e complesse convenzioni narrative, le quali mantengono un rapporto di filiazione indiretto − per una via che potremmo definire denegativa − con quelle del romanzo tradizionale.

Matrix Designs and Methods for Secure and Efficient Compressed Sensing

The idea of balancing the resources spent in the acquisition and encoding of natural signals strictly to their intrinsic information content has interested nearly a decade of research under the name of compressed sensing. In this doctoral dissertation we develop some extensions and improvements upon this technique's foundations, by modifying the random sensing matrices on which the signals of interest are projected to achieve different objectives. Firstly, we propose two methods for the adaptation of sensing matrix ensembles to the second-order moments of natural signals. These techniques leverage the maximisation of different proxies for the quantity of information acquired by compressed sensing, and are efficiently applied in the encoding of electrocardiographic tracks with minimum-complexity digital hardware. Secondly, we focus on the possibility of using compressed sensing as a method to provide a partial, yet cryptanalysis-resistant form of encryption; in this context, we show how a random matrix generation strategy with a controlled amount of perturbations can be used to distinguish between multiple user classes with different quality of access to the encrypted information content. Finally, we explore the application of compressed sensing in the design of a multispectral imager, by implementing an optical scheme that entails a coded aperture array and Fabry-Pérot spectral filters. The signal recoveries obtained by processing real-world measurements show promising results, that leave room for an improvement of the sensing matrix calibration problem in the devised imager.