O amplo emprego do exame de DNA em ações de investigação de paternidade levou à divulgação maciça de sua eficácia pelos meios de comunicação que acabou por lhe dar uma aura de infalibilidade, colocando em descrédito os métodos analíticos mais antigos. Enfocado pela mídia como técnica suprema, foram omitidas do grande público as limitações existentes quando aplicada à Criminalística, seu alto custo e a complexidade dos processos técnicos exigidos para que sejam auferidos resultados confiáveis. No meio jurídico brasileiro, o tema é ainda discutido de forma superficial, marginalizando os operadores do direito dos conhecimentos técnico-científicos necessários para a interpretação dos resultados probabilísticos oferecidos pelos exames de DNA. Este trabalho procura, de certa forma, diminuir esta lacuna técnico-científica e esclarecer os reais alcances e limitações da aplicação desta técnica nas investigações forenses como auxiliar na elucidação de crimes e na identificação de pessoas. Inicia-se pelo estudo da evolução das técnicas empregadas na Medicina Forense para a identificação humana, discutindo-se a propalada sobrepujança da análise de DNA em relação aos tradicionais exames periciais. É feita uma abordagem sobre o desenvolvimento da Biologia Molecular, principiando-se pelo estudo da estrutura do DNA e pela forma de transmissão da informação genética, para, em seguida, tratar da detecção de polimorfismos presentes nesta molécula propiciadores, em última instância, da obtenção de padrões genéticos indivíduo-específicos que vêm sendo empregados na identificação de suspeitos em casos de crimes sexuais; na identificação de cadáveres de vítimas de crimes ou de grandes catástrofes; e no estabelecimento de vínculo entre suspeitos e locais de crime, entre um local de crime e outro, e entre instrumento lesivo e vítima. Dá-se também grande ênfase à coleta de materiais e as precauções para garantir a cadeia de custódia das amostras que serão estudadas, ressaltando-se ainda aspectos éticos e jurídicos que envolvem a questão da coleta de materiais biológicos de suspeitos à luz do direito brasileiro. São também abordados os procedimentos laboratoriais utilizados para a extração, quantificação, amplificação e detecção do DNA dos materiais analisados, bem como os métodos estatísticos empregados para a correta interpretação dos resultados auferidos e as recomendações existentes para elaboração do laudo pericial e para o necessário controle de qualidade das análises de DNA. São discutidos aspectos atinentes ao uso das informações sobre o DNA, quer em suas repercussões sociais quer como prova na justiça penal, pela abordagem de características de seu contraditório e de seu real valor para a formação da culpabilidade. É ainda apresentado o trabalho pericial realizado no Laboratório de DNA do Instituto de Criminalística de São Paulo e também exposto um estudo estatístico sobre a eficácia técnica das análises realizadas neste laboratório. Conclui-se que a análise de DNA, mesmo sendo uma poderosa ferramenta, está longe de ser uma condição sine qua non em estudos forenses. A prova de DNA deve ser sempre considerada dentro de um conjunto de variadas evidências e o papel do geneticista forense não é o de fazer presunções de culpabilidade ou de inocência, mas o de fornecer informações exatas para melhor aplicação da justiça. / The wide application of the DNA exam in paternity investigation led to the massive divulgation of its efficiency through the communication channels, earning it a reputation of infallible result, and jeopardizing the credit of older analytical methods. While focused by the media as the most supreme technique, several limitations were omitted regarding its use in criminal matters, such as its high cost and the complexity of technical processes demanded for trustworthy results. The theme is still discussed in a superficial way among the Brazilian juridical scenario, which leaves the law related individuals with a lack of technical and scientific knowledge required to the interpretation of results offered by DNA exams. The goal of this report is to, in a way, diminish this technical and scientific gap and clarify the real accomplishments and limitations of this technique, while applied to forensic investigations as an auxiliary alternative to crime solving and people identifying. We begin with the study on the evolution of the techniques applied in Legal Medicine to human identification, discussing the surpass of DNA analysis in relation to other traditional exams. The development of Molecular Biology is featured with basis on the DNA structure and the way the genetic information is transmitted, followed by the polymorphisms detection in this molecule and obtainment of specific genetic patterns which have been used for identifying suspects of sexual crimes; identification of crime and catastrophe victims, and in the establishment of a link between suspects and crime scenes, one crime scene and another, and a wound object and a victim. Great emphasis is given to the collecting of material and precaution used to ensure the custody of samples to be analysed, enhancing the ethic and legal aspects involving the collection of biological material of suspects brought to light as per the Brazilian Law. Laboratory procedures utilized to the extraction, amplifying and detection of DNA analysed material are outlined, and statistics methods applied to the correct interpretation of results and existing recommendations to elaborate the expert report, and to the necessary quality control of DNA analysis. Several aspects referent to the use of information about DNA are discussed, as whether in relation to its social repercussions or as a penal proof, through the characteristics of its contradictory and real value to elaborate culpability. An expert essay formulated at the São Paulo Criminal Institute DNA Laboratory is presented along with a statistics study on the technical efficacy of samples analysis made in that lab. The conclusion is that the DNA analysis, despite being a powerful tool, is far from being a sine qua non condition in forensic studies. The DNA proof must always be considered within an ensemble of various evidences, and the role of the legal genetic expert is not to make presumptions of culpability of innocence, but to provide accurate information to help the applicable law.

Submitted by JÚLIO HEBER SILVA (julioheber@yahoo.com.br) on 2017-04-11T19:28:47Z No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-04-12T14:32:03Z (GMT) No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-04-12T14:32:03Z (GMT). No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-03-07 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / The process of developing computer systems takes into account many stages, in which some are more necessary than others, depending on the purpose of the application. The implementation stage is always necessary, indisputably. Sometimes the requirements analysis and testing phases are neglected. And, generally, the part of formal verification correctness is intended for few applications. The use of model checkers has been exploited in the task of validating a behavioral specification in its appropriate level of abstraction, notably specifications validation of critical systems, especially when they involve the preservation of human life, when the existence of errors entails huge financial loss or when deals with information security. Therefore, it proposes to apply formal verification techniques in the validation of the vehicular safety system Avoiding Doored System, considered as critical, in order to verify if the implemented system faithfully meets the requirements for it proposed. For that, it was used as a tool to verify its correctness the Specification and Verification System - PVS, detailing and documenting all the steps employed in the process of specification and formal verification. K / O processo de desenvolvimento de sistemas computacionais leva em conta muitas etapas, nos quais umas são tidas mais necessárias que outras, dependendo da finalidade da aplica- ção. A etapa de implementação sempre é necessária, indiscutivelmente. Por vezes as fases de análise de requisitos e de testes são negligenciadas. E, geralmente, a parte de verifica- ção formal de corretude é destinada a poucas aplicações. O uso de verificadores de modelos tem sido explorado na tarefa de validar uma especificação comportamental no seu nível adequado de abstração, sobretudo, na validação de especificações de sistemas críticos, principalmente quando estes envolvem a preservação da vida humana, quando a existência de erros acarreta enorme prejuízo financeiro ou quando tratam com a segurança da informa- ção. Diante disso, se propõe aplicar técnicas de verificação formal na validação do sistema de segurança veicular Avoiding Doored System, tido como crítico, com o intuito de atestar se o sistema implementado atende, fielmente, os requisitos para ele propostos. Para tal, foi utilizada como ferramenta para a verificação de sua corretude o Specification and Verification System - PVS, detalhando e documentando todas as etapas empregadas no processo de especificação e verificação formal. Pal

Neste trabalho, apresentamos um método computacional rigoroso para a demonstração de existência de órbitas periódicas de alguns sistemas de equações diferenciais ordinárias com campo autônomo do tipo polinomial. Mostraremos que o problema de encontrar órbitas periódicas para esses sistemas de equações é equivalente a buscar por raízes de certas funções definidas no espaço de Banach das sequências com decaimento algébrico. O método pode ser dividido em duas etapas. Na primeira, buscamos numericamente por soluções periódicas aproximadas. Na segunda, mostraremos a existência de uma órbita periódica numa vizinhança da curva encontrada numericamente. O rigor das verificações computacionais é garantido pelo uso de aritimética intervalar. / In this work, we present a rigorous computational method for proving the existence of periodic orbits of some systems of ordinary differential equations with autonomous vector field of polynomial type. We show that the problem of finding periodic orbits for these systems is equivalent to check for roots of certain functions defined in the Banach space of sequences with algebraic decay. The method can be divided into two steps. First, we seek, numerically, to approximated periodic solutions. Then, we show the existence of a periodic orbit in a neighborhood of the curve numerically found in the previous stage. The accuracy of the computational verifications is guaranteed by the use of interval arithmetic.

Submitted by Geandra Rodrigues (geandrar@gmail.com) on 2018-06-15T14:13:38Z No. of bitstreams: 0 / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2018-06-27T14:02:06Z (GMT) No. of bitstreams: 0 / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2018-06-27T14:02:53Z (GMT) No. of bitstreams: 0 / Made available in DSpace on 2018-06-27T14:02:53Z (GMT). No. of bitstreams: 0 Previous issue date: 2018-03-11 / O presente trabalho tem como tema a possibilidade de controle lógico-racional do juízo fático por meio da incidência da teoria dos standards probatórios, a qual é problematizada no contexto da responsabilidade civil do médico. Tem por objetivos centrais refletir acerca de qual standard de prova deverá incidir em ações de responsabilidade civil do médico, bem como observar se há um grau de suficiência de prova sendo exigido pelo TJMG e TJRS para aceitar como racionalmente comprovada a culpa nesse tipo de demanda. Esse estudo foi realizado não apenas mediante averiguação bibliográfica de doutrina nacional e estrangeira, mas também por meio de uma pesquisa empírica de natureza qualitativa das decisões cíveis dos Tribunais de Justiça do Estado de Minas Gerais e do Estado do Rio Grande do Sul que lidam com a prova da culpa e dos demais elementos ensejadores da responsabilidade civil do médico para que, assim, fosse possível compreender, através da análise do grau de prova das narrativas jurisprudenciais, como os juízes estão aferindo a suficiência do conjunto probatório quanto à comprovação da hipótese fática, diante dos elementos de juízo disponíveis. Adota-se como referencial teórico o princípio da persuasão racional, conceito construído gradativamente pela doutrina ao longo dos anos e interpretado, segundo a concepção atual de racionalidade que lhe subjaz, como liberdade relativa de valoração das provas, realizada dentro de parâmetros lógico-racionais entre os quais se incluem os standards probatórios. Essa pesquisa é de grande valia social e acadêmica, na medida em que traz uma perspectiva inovadora ao terreno da prova e da convicção judicial, proporcionando inegável desenvolvimento jurisprudencial e doutrinário em nosso país, o que nos torna assim, mais próximos de alcançar decisões mais justas. Conclui-se, sob a ótica do referencial teórico previamente estabelecido, que a pesquisa teórica e a visão crítica sobre o resultado da pesquisa empírica confirmaram a hipótese no sentido de que ao julgamento fático em ações de responsabilidade civil médica incidirá o standard da prova clara e convincente enquanto critério de julgamento, o qual não apenas indica o grau de prova a ser necessariamente satisfeito para comprovar a culpa do médico, como também proporciona maior controle da motivação judicial sobre os fatos, dotando assim de maior legitimidade e racionalidade as decisões judiciais. / The present study has as its theme the possibility of logical-rational control of the phatic judgment through the incidence of the standard of proof theory, which is problematized in the context of medical civil responsibility. It aims are to reflect on which standard of proof should be involved in actions of medical civil responsibility, as well as to observe if there is a degree of sufficiency of proof being required by the TJMG and TJRS to accept as rationally proven the fault in this type of demand. It was carried out not only through a bibliographic examination of national and foreign doctrine, but also through a qualitative empirical research of civil decisions of the Courts of Justice of the State of Minas Gerais and of the State of Rio Grande do Sul that deal with the proof of fault and other elements that give rise to medical civil responsibility, so that it would be possible to understand, through the analysis of the degree of proof of these jurisprudential narratives, how the judges are assessing the sufficiency of the probative set to prove the factual hypothesis, in view of the available evidence. It adopts as theoretical reference the principle of rational persuasion, a concept built gradually by the doctrine over the years and interpreted, according to the current conception of rationality that underlies it, as relative freedom of evaluation of the tests, carried out within rational-rational parameters between which include the standards of proof. This research is of great social and academic value, since it brings an innovative perspective to the field of proof and judicial conviction, providing undeniable jurisprudential and doctrinal development in our country, which makes us closer to reaching fairer decisions. It concludes, from the perspective of the previously established theoretical framework, that the theoretical research and the critical view on the result of the empirical research made possible the confirmation of the hypothesis that the standard of proof to be applied to the factual judgment in medical civil responsibility is the clear and convincing one, as a criterion of judgment, which will not only indicate the degree of proof to be necessarily satisfied to prove the doctor's fault, but also will provide better control of the judicial motivation on the facts, thus giving greater legitimacy and rationality to judicial decisions.

The aim of this study is to investigate if there is a way a computer can accurately and automatically react on altered configuration file(s) with a minimum of resource utilization and by what means the developer(s) of an application can perform a check of the altered configuration file for their application. In a typical GNU/Linux installation the configuration files are literally counted by the thousands, monitoring these files is a task that for the most part exceeds any system administrator's abilities. Each file has its own syntax that needs to be known by the administrator. Either one of these two tasks could give any system administrator nightmares concerning the difficulty level especially when both tasks are combined. The system administrator could attempt to automate the monitoring tasks together with the syntax checking. There are some tools in the repositories of each distribution for monitoring files but none that lets one monitor and take (predefined or user defined) actions based on what the file monitor reports, the type of file and its contents. A complete tool is not presented in this study, merely a proof of concept that monitoring and taking actions especially with version 2.6.13 (or newer) kernel of GNU/Linux with plugins are quite possible with relatively small computer resource. During this study some questions arose that are worth taking into consideration when a complete monitoring tool is to be developed, amongst others they are: add a trusted user, add both textual and graphical user interface, monitor more than one file path. This study was performed on GNU/Linux CentOS 6 distribution, all programming was done in BASH with an effort to minimize used/installed programs.

Les croissances constantes de l’Internet et des services associés ont conduit à des problématiques naturellement liées au domaine de la cryptographie, parmi lesquelles l’authentification et le respect de la vie privée des utilisateurs. L’utilisation désormais commune d’appareils connectés (smartphone, tablette, montre, …) comme moyen d’authentification amène à considérer la génération et/ou la gestion de clés cryptographiques par de tels appareils pour répondre à ces besoins. Les résonances cryptographiques identifiées de ces deux cas d’étude sont respectivement le domaine des Fuzzy Extractors (« Extracteurs de Flous » en français) et les schémas de signature de groupe. D’une part, cette thèse présente alors le premier Fuzzy Extractror non basé sur la distance de Hamming à être réutilisable (dans le modèle de l’oracle aléatoire non programmable). Ce faisant, nous avons alors pu concevoir un module de génération de clés cryptographiques permettant d'authentifier un utilisateur à partir des ses appareils. D’autre part, deux schémas de signature de groupe basés sur la théorie des codes, respectivement en métrique de Hamming et en métrique rang sont également proposés. Ces deux schémas constituent des alternatives crédibles aux cryptosystèmes post-quantiques équivalents basés sur les réseaux euclidiens. / Internet constant growth has naturally led to cryptographic issues such as authentication and privacy concerns. The common usage of connected devices (smartphones, tablet, watch, …) as authentication means made us consider cryptographic keys generations and/or managements from such devices to address aforementioned needs. For such a purpose, we identified fuzzy extractors and group signature schemes. On the one hand, this thesis then presents the first reusable fuzzy extractor based on set difference metric (in the nonprogrammable random oracle). In so doing, we were able to design a key generation module performing authentication from users’ devices. On the other hand, we came up with two group signature schemes, respectively based on Hamming and rank metrics, that seriously compete with post-quantum concurrent schemes based on lattices.

Le problème général de la preuve de propriétés de programmes impératifs est indécidable. Pour deslangages de programmation et de propriétés plus restrictifs, des sous-problèmes décidables sontconnus. En pratique, grâce à des heuristiques, les outils de preuve de programmes automatisent despreuves qui sortent du cadre théorique de ces sous-problèmes décidables connus. Nous illustronscette réussite pratique en construisant un catalogue de preuves, pour des programmes et despropriétés de nature similaire et de complexité croissante. Ces programmes sont principalementdes générateurs de cartes combinatoires.Ainsi, ce travail contribue aux domaines de recherche de la combinatoire énumérative et dugénie logiciel. Nous distribuons une bibliothèque C de générateurs exhaustifs bornés de tableauxstructurés, formellement spécifiés en ACSL et vérifiés avec le greffon WP de la plateforme d’analyseFrama-C. Nous proposons également une méthodologie de test qui facilite la preuve interactive enCoq, une étude formelle des cartes originale, et de nouveaux résultats en combinatoire énumérative. / The general problem of proving properties of imperative programs is undecidable. Some subproblems– restricting the languages of programs and properties – are known to be decidable. Inpractice, thanks to heuristics, program proving tools sometimes automate proofs for programs andproperties living outside of the theoretical framework of known decidability results. We illustrate thisfact by building a catalog of proofs, for similar programs and properties of increasing complexity. Mostof these programs are combinatorial map generators.Thus, this work contributes to the research fields of enumerative combinatorics and softwareengineering. We distribute a C library of bounded exhaustive generators of structured arrays, formallyspecified in ACSL and verified with the WP plugin of the Frama-C analysis platform. We also proposea testing-based methodology to assist interactive proof in Coq, an original formal study of maps, andnew results in enumerative combinatorics.

Quel étrange personnage que le commissionnaire de transport ! Cet acteur majeur du monde des transports est à l’origine de nombreuses controverses doctrinales et d’un abondant contentieux judiciaire. Professionnel chargé d’organiser le transport des marchandises pour le compte d’un donneur d’ordre, il supporte une double responsabilité, de son fait personnel et du fait de tous les prestataires qu’il se substitue dans l’exécution de sa mission. Si le recours à la commission de transport est très fréquent, c’est parce qu’elle offre de garanties intéressantes aux clients, notamment la prise en charge intégrale de l’organisation du transport avec les risques qu’elle comporte. Cependant, en analysant attentivement la jurisprudence de ces dernières années, on a pu observer que la responsabilité de la plupart des commissionnaires de transport a été très lourdement appréciée. Le motif souvent retenu étant la faute personnelle, facilement assimilée à la faute lourde par les juges, avec pour conséquence la perte du bénéfice des limitations d’indemnités pour ce dernier. Que recouvre précisément la faute du commissionnaire de transport ? Sur ce point, on a assisté à une jurisprudence inflationniste notamment sur le devoir de conseil, les contours de cette notion n’étant pas clairement définis. La situation était devenue si préoccupante que les pouvoirs publics ont cru bon d’intervenir à travers deux réformes majeures. D’abord par la loi du 8 décembre 2009 avec l’introduction du nouvel article L.133-8 du Code de commerce, qui conditionne dorénavant l’exclusion des limitations d’indemnités à la preuve d’une faute dolosive ou inexcusable du commissionnaire de transport ou du transporteur. Ensuite par l’adoption du contrat type commission de transport (en vigueur depuis 2013). Ce contrat type, fruit d’une longue et laborieuse négociation entre les professionnels de ce secteur, encadre sérieusement la responsabilité personnelle du commissionnaire de transport. Comment appréhender alors la faute du commissionnaire de transport à la lumière de ces réformes ? C’est à cette question essentielle que ce travail va tenter d’apporter des éléments de réponses en s’appuyant sur les textes en vigueur et de la pratique observée dans les prétoires. / What a strange character the freight forwarder (Agent) is ! This leading player of the world of transport is the source of several doctrinal debates and implies a plentiful judicial dispute. Professional appointed to organize the transport of the goods on behalf of a contractor, he bears a double responsibility, of his personal fact and because of all the persons receiving benefits for whom he substitutes itself in the execution of his mission. If the appeal to the committee of transport is very frequent, it is due to the interesting guarantees it offers to the customers, in particular the complete coverage of the organization of the transport with the risks which it involves. However, by carefully analyzing the jurisprudence of recent years, it has been observed that the responsibility for most freight forwarders was very heavily estimated. The often held motive being the personal fault easily likened to the serious offence by the judges, involving the loss of the profit of the limitations of compensations for the latter. What does exactly the fault of the forwarder cover? On this point, we attended an inflationary jurisprudence in particular on the duty of advice, the outlines of this notion not being clearly defined. The situation had become so worrisome as public authorities saw fit to intervene through two fundamental reforms. At first by the law of December 8th, 2009 with the introduction of the new article L.133-8 of the Commercial law, which conditions from now on the exclusion of the limitations of compensations in the proof of a dolosive or unforgivable fault of the agent of transport or the carrier. And then by the adoption of the standard commission contract of transport (in force since 2013). This standard contract, fruit of a long and laborious negotiation between the professionals of this sector, frames seriously the personal liability of the forwarder. How to identify then the fault of the forwarder in the light of these reforms? It is to this essential question that this work is going to try to bring elements of answers based on the current texts and the practice observed in the courts of justice.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

Cette thèse étudie la théorie de la correspondance et la théorie des preuves pour la logique modale monotone et les logiques qui en sont proches.La première partie de la thèse établit une connexion formelle entre la théorie de la correspondance algorithmique et des résultats de caractérisation duale pour les treillis finis, similaire à la caractérisation par Nation d'une hiérarchie de variétés de treillis qui généralise les treillis distributifs. Cette connexion formelle est établie en utilisant la logique modale monotone. Nous adaptons l'algorithme ALBA pour la correspondance à l'environnement de la logique modale monotone, et nous utilisons un encodage, induit par une dualité, des treillis finis sous forme de 'neighbourhood frames' pour traduire les termes de la théorie des treillis en formules de la logic modal monotone.La deuxième partie de la thèse étend la théorie des 'display calculi' à la logique Baltag-Moss-Solecki pour les actions épistémiques et la connaissance (Epistemic Actions and Knowledge), à la logique modale monotone et à la logique propositionnelle dynamique (PDL). Nos résultats incluent plusieurs méta-théorèmes d'élimination de la coupure qui généralisent le théorème original de Belnap dans des dimensions différentes et indépendantes. Les deux principales généralisations des 'display calculi' traitées dans la thèse sont : la généralisation d'une théorie pour les langages ne contenant qu'un seul type à une théorie pour les langages contenant plusieurs types, et la généralisation d'une théorie pour les calculs satisfaisant la propriété de 'display' aux calculs ne la satisfaisant pas. / The present thesis focuses on Monotone Modal Logic and closely related logics from the point of view of Correspondence Theory and Proof Theory.The first part of the thesis establishes a formal connection between algorithmic corre- spondence theory and certain dual characterization results for finite lattices, similar to Nation's characterization of a hierarchy of pseudovarieties of finite lattices progressively generalizing finite distributive lattices. This formal connection is established through monotone modal logic. Specifically, we adapt the correspondence algorithm ALBA to the setting of monotone modal logic, and we use a certain duality-induced encoding of finite lattices as monotone neighbourhood frames to translate lattice terms into formulas in monotone modal logic.The second part of the thesis extends the theory of display calculi to Baltag-Moss- Solecki's logic of Epistemic Actions and Knowledge (EAK), Monotone Modal Logic (MML), and Propositional Dynamic Logic (PDL). Our results include several cut-elimination metatheorems, which generalize the original metatheorem of Belnap in different and mutually independent dimensions. The two main generalizations of display calculi treated in the thesis are: the generalization from single type to multi-type languages, and from the full or relativized display property to no display property.