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.

Il Pluralismo tra Democrazia ed Autoritarismo: Il Caso Russo

The research explores the mechanisms in the formation and consolidation of a new regime which combines democratic and authoritarian features; it has emerged as result of democratization processes affecting different world areas in recent years. The study analyses a case of great international significance, post-communist Russia: here internal factors strongly prevail in front of the external variables of democratic imitation and contagion, thus showing to what extent Russia differs from other political contexts. The study intends to examine the strategies used by this regime to solve internal conflicts and become stable in spite of the democratizing pressures coming from outside. Indeed, the literature about political transformations has shown the problems in analyzing these polities together with the need to examine their peculiarities more in depth. In this perspective, the first section focuses on the dynamics of State-building in Russia as a fundamental process in tracing the specific characteristics of the current regime: particularly, it is suggested that the State dimension comes out as crucial in determining the level of political and social pluralism accepted in post-Soviet Russia. This argument is worked out in the second section, which analyses the main mechanisms used by the incumbents to limit and control pluralism within the two arenas of political competition and civil society, from where the major threats to the status quo are supposed to come. The main hypothesis is that the leadership interventions in these spheres during the last ten years have shaped a regime which can be characterized as a new type of authoritarianism: with respect to traditional authoritarian forms a certain degree of political contestation is accepted, visible in the presence of a multiparty system, semi-competitive elections and of the several representatives of civil society. Yet, this diversity is curbed basically in two different ways: from one hand the incumbents provide support to political and social actors who sponsor government politics (see the party of power and pro-Kremlin movements). From the other they use some non coercive forms of control and restriction (in legislation, in political elections) against those actors who promote values and priorities opposed to the official ones.

La coazione all'adempimento mediante la tecnica delle misure coercitive indirette

La tesi intende offrire una riflessione in merito all’utilizzo della tecnica delle misure coercitive indirette quali strumenti di coartazione della volontà dell’obbligato al fine di indurlo all’esatto adempimento in presenza di statuizioni giudiziali il cui contenuto si sostanzi in prestazioni a carattere infungibile o in un dovere di astensione dal porre in essere determinati comportamenti, che non possono trovare esecuzione secondo le ordinarie forme previste dal Libro Terzo del Codice di procedura civile. Il lavoro prende le mosse dall'analisi storico-comparatistica dello sviluppo dell'esecuzione processuale indiretta nei principali ordinamenti giuridici europei, per poi soffermarsi sulle singole misure coercitive indirette disciplinate dal legislatore italiano nel corso degli anni al fine di far fronte alle esigenze di tutela emergenti in specifici settori del diritto. Segue un'attenta disamina in ordine alla disposizione di cui all'art. 614-bis c.p.c., con cui è stata introdotta per la prima volta nel nostro ordinamento una misura coercitiva indiretta a carattere generale in materia di esecuzione degli obblighi di fare infungibile e di non fare.

Arresto e fermo: Prassi applicative e prospettive di riforma

Il presente lavoro ha ad oggetto l’esame della disciplina dell’arresto in flagranza e del fermo di indiziato di delitto: istituti profondamente “utili” e “d’impatto” (anche mass-mediatico) perché ontologicamente tesi, soprattutto il primo, all’immediata repressione del fenomeno criminale. Scopo e ragione di questo studio, è dunque l’individuazione di altre e più profonde finalità di tali istituti, passando per una piena comprensione del ruolo loro assegnato nel vigente impianto codicistico. La ricerca, dunque, si è sviluppata lungo tre direttrici, ciascuna rappresentata – anche dal punto di vista grafico-strutturale – nelle tre parti cin cui è diviso l’elaborato finale e ciascuna singolarmente riferibile, in un’immaginaria linea del tempo, allo ieri (e ai principi), all’oggi e al domani della disciplina delle misure coercitive di polizia giudiziaria. Nella prima parte, infatti, partendo dall’analisi storica degli istituti in esame, si è proceduto all’esame della disciplina e della giurisprudenza costituzionale in tema di strumenti di polizia giudiziari provvisoriamente limitativi della libertà personale; l’obiettivo primo di tale approfondimento, cui poi sarà informato l’analisi della dinamica degli istituti, è proprio l’individuazione delle finalità – conformi a Costituzione – dell’arresto e del fermo di indiziato di delitto. Seguirà l’analisi del concetto di libertà personale, e dei margini consentiti per la sua limitazione, in seno al sistema della Convenzione europea per la salvaguardia dei diritti dell’uomo. La seconda parte contiene un’analisi critica degli istituti dell’arresto in flagranza, del fermo di indiziato di delitto e dell’arresto urgente a fini estradizionale. Infine, la terza e ultima parte ha ad oggetto l’ulteriore di linea di ricerca che si è sviluppata a mo’ di conclusione delle predette analisi, riguardante la possibilità di utilizzare lo strumento del fermo, ampliandone le maglie applicative, come viatico per l’introduzione del contraddittorio anticipato rispetto all’applicazione delle misure cautelari personali