bibliography.bib

@article
{
    Appel,

    author          = {Kenneth Appel and Wolfgang Haken},
    journal         = {Bulletin of the American Mathematical Society},
    title           = {Every map is four colourable},
    doi             = {https://doi.org/10.1090/S0002-9904-1976-14122-5},
    year            = {1976}
}

@book
{
    Aristotle,

    address        = {Cambridge},
    author         = {Aristóteles},
    publisher      = {Harvard University Press},
    note           = {Tradução de Harold Percy Cooke, Hugh Tredennick e Edward Seymour Forster},
    title          = {Organon},
    year           = {1938}
}

@article
{
    Barcan,

    author          = {Ruth Barcan Marcus},
    journal         = {The Journal of Symbolic Logic},
    title           = {The deduction theorem in a functional calculus of first order based on strict implication},
    year            = {1946}
}

@article
{
    Beziau,

    author          = {Jean-Yves Béziau},
    journal         = {Logica},
    title           = {Universal logic},
    year            = {1994}
}

@inproceedings
{
    Beziau-B,

    address         = {Basileia},
    author          = {Jean-Yves Béziau},
    booktitle       = {Logica Universalis},
    publisher       = {Birkh{\"a}user Basel},
    title           = {From consequence operator to universal logic: a survey of general abstract logic},
    doi             = {https://doi.org/10.1007/978-3-7643-8354-1_1},
    year            = {2007}
}

@article
{
    Benton,

    author          = {Peter Nicholas Benton and Gavin Mark Bierman and Paiva, Valeria Correa Vaz de},
    journal         = {Journal of Functional Programming},
    title           = {Computational types from a logical perspective},
    doi             = {https://doi.org/10.1017/S0956796898002998},
    year            = {1998}
}

@book
{
    Blackburn,

    author         = {Patrick Blackburn and Maarten de Rijke and Yde Venema},
    publisher      = {Cambridge University Press},
    title          = {Modal logic},
    year           = {2001}
}

@book
{
    Brouwer-A,

    author         = {Luitzen Egbertus Jan Brouwer},
    publisher      = {Maas \& van Suchtelen},
    title          = {Over de grondslagen der wiskunde},
    year           = {1907}
}

@article
{
    Brouwer-B,

    author          = {Luitzen Egbertus Jan Brouwer},
    journal         = {Tijdschrift voor Wijsbegeerte},
    title           = {De onbetrouwbaarheid der logische principes},
    year            = {1908}
}

@book
{
    Chellas,

    author         = {Brian Farrell Chellas},
    publisher      = {Cambridge University Press},
    title          = {Modal logic: an introduction},
    year           = {1980}
}

@book
{
    Chlipala,

    author         = {Adam Chlipala},
    publisher      = {The Massachusetts Institute of Technology Press},
    title          = {Certified programming with dependent types},
    isbn           = {9780262545747},
    year           = {2022}
}

@article
{
    Coniglio,

    author          = {Marcelo Esteban Coniglio},
    journal         = {Manuscrito},
    title           = {Towards a stronger notion of translation between logics},
    year            = {2005}
}

@article
{
    Curry-A,

    author          = {Haskell Brooks Curry},
    journal         = {Journal of Symbolic Logic},
    title           = {The elimination theorem when modality is present},
    doi             = {https://doi.org/10.2307/2266613},
    year            = {1952}
}

@book
{
    Curry-B,

    author         = {Haskell Brooks Curry},
    location       = {Notre Dame},
    publisher      = {University of Notre Dame Press},
    title          = {A theory of formal deducibility},
    doi            = {https://doi.org/10.2307/2270991},
    year           = {1957}
}

@article
{
    Došen,

    author          = {Kosta Došen},
    journal         = {Logique et Analyse},
    title           = {Modal translations and intuitionistic double negation},
    year            = {1986}
}

@inproceedings
{
    Fairtlough,

    author          = {Matt Fairtlough and Michael Mendler},
    booktitle       = {Computer Science Logic},
    publisher       = {Springer},
    title           = {An intuitionistic modal logic with applications to the formal verification of hardware},
    doi             = {https://doi.org/10.1007/BFb0022268},
    year            = {1995}
}

@article
{
    Font,

    author          = {Josep Maria Font and Ramon Jansana and Don Leonard Pigozzi},
    journal         = {Studia Logica},
    title           = {A survey of Abstract Algebraic logic},
    doi             = {https://doi.org/10.1023/A:1024621922509},
    year            = {2003}
}

@incollection
{
    Franks,

    author          = {Curtis Franks},
    booktitle       = {The {Stanford} Encyclopedia of Philosophy},
    publisher       = {Stanford University},
    title           = {{Propositional Logic}},
    url             = {https://plato.stanford.edu/entries/logic-propositional/},
    year            = {2024}
}

@book
{
    Frege,

    author         = {Gottlob Frege},
    location       = {Halle an der Saale},
    publisher      = {Verlag von Louis Nebert},
    title          = {Begriffsschrift: {E}ine der arithmetischen nachgebildete {F}ormelsprache des reinen {D}enkens},
    year           = {1879}
}

@article
{
    Mendler,

    author          = {Matt Fairtlough and Michael Mendler},
    journal         = {Information and Computation},
    title           = {Propositional lax logic},
    doi             = {https://doi.org/10.1006/inco.1997.2627},
    year            = {1997}
}

@article
{
    Girard,

    author          = {Jean-Yves Girard},
    journal         = {Theoretical Computer Science},
    title           = {Linear logic},
    issn            = {0304-3975},
    doi             = {https://doi.org/10.1016/0304-3975(87)90045-4},
    year            = {1987}
}

@article
{
    Goedel,

    author          = {Kurt Gödel},
    journal         = {Ergebnisse eines {M}athematischen {K}olloquiums},
    title           = {Eine {I}nterpretation des intuitionistischen {A}ussagenkalküls},
    year            = {1933}
}

@article
{
    Gonthier,

    author          = {Georges Gonthier},
    journal         = {Notices of the American Mathematical Society},
    title           = {Formal proof: the four-color theorem},
    year            = {2008}
}

@article
{
    Hakli,

    author          = {Raul Hakli and Sara Negri},
    journal         = {Synthese},
    title           = {Does the deduction theorem fail for modal logic?},
    doi             = {https://doi.org/10.1007/s11229-011-9905-9},
    year            = {2012}    
}

@article
{
    Hilbert-A,

    author          = {David Hilbert},
    journal         = {Mathematische Annalen},
    title           = {{Über das Unendliche}},
    doi             = {https://doi.org/10.1007/BF01206605},
    year            = {1926}    
}

@book
{
    Hilbert-B,

    author          = {David Hilbert},
    publisher       = {Springer},
    title           = {{Die Grundlagen der Mathematik}},
    doi             = {https://doi.org/10.1007/978-3-663-16102-8},
    year            = {1928}    
}

@article
{
    Kolmogorov,

    author          = {Andrej Nikolaevič Kolmogorov},
    journal         = {Matematičeskij Sbornik},
    title           = {On the principle of the excluded middle},
    year            = {1925}    
}

@book
{
    Langford,

    address        = {Nova York},
    author         = {Clarence Irving Lewis and Cooper Harold Langford},
    publisher      = {Century},
    title          = {Symbolic logic},
    year           = {1932}
}

@article
{
    Lewis,

    author          = {Clarence Irving Lewis},
    issn            = {0026-4423},
    journal         = {Mind},
    title           = {Implication and the algebra of logic},
    doi             = {https://doi.org/10.1093/mind/XXI.84.522},
    year            = {1912}
}

@article
{
    Marcus,

    author          = {Ruth Barcan Marcus},
    journal         = {The Journal of Symbolic Logic},
    title           = {Strict implication, deducibility and the deduction theorem},
    year            = {1953}
}

@article
{
    McKinsey,

    author          = {John Charles Chenoweth McKinsey and Alfred Tarski},
    journal         = {The Journal of Symbolic Logic},
    title           = {Some theorems about the sentential calculi of {L}ewis and {H}eyting},
    year            = {1948}
}

@article
{
    Moggi,

    author         = {Eugenio Moggi},
    title          = {Notions of computation and monads},
    journal        = {Information and Computation},
    doi            = {https://doi.org/10.1016/0890-5401(91)90052-4},
    issn           = {0890-5401},
    year           = {1991}
}

@inproceedings
{
    Nunes,

    author         = {Miguel Alfredo Nunes and Karina Girardi Roggia and Paulo Henrique Torrens},
    booktitle      = {Proceedings of the XXVI Brazilian Symposium on Formal Methods},
    title          = {Soundness-preserving fusion of modal logics in \textsc{coq}},
    year           = {2024}
}

@article
{
    Pfenning,

    author         = {Frank Pfenning and Rowan Davies},
    title          = {A judgmental reconstruction of modal logic},
    journal        = {Mathematical Structures in Computer Science},
    doi            = {https://doi.org/10.1017/S0960129501003322},
    year           = {2001}
}

@article
{
    Reynolds,

    author         = {John Charles Reynolds},
    title          = {The discoveries of continuations},
    journal        = {Higher-Order and Symbolic Computation},
    doi            = {https://doi.org/10.1007/BF01019459},
    year           = {1993}
}

@book
{
    Russel-A,

    author         = {Alfred North Whitehead and Bertrand Russell},
    address        = {Cambrige},
    publisher      = {Cambridge University Press},
    title          = {Principia mathematica},
    year           = {1910},
    note           = {Volume 1}
}

@book
{
    Russel-B,

    author         = {Alfred North Whitehead and Bertrand Russell},
    address        = {Cambrige},
    publisher      = {Cambridge University Press},
    title          = {Principia mathematica},
    year           = {1911},
    note           = {Volume 2}
}

@book
{
    Russel-C,

    author         = {Alfred North Whitehead and Bertrand Russell},
    address        = {Cambrige},
    publisher      = {Cambridge University Press},
    title          = {Principia mathematica},
    year           = {1912},
    note           = {Volume 3}
}

@mastersthesis
{
    Sehnem,

    author         = {Alexandre Sehnem},
    school         = {Universidade do Estado de Santa Catarina},
    title          = {Formalização da tradução das lógicas clássica e intuicionista para a lógica linear em \textsc{coq}},
    year           = {2023},
    type           = {Trabalho de conclusão de curso}
}

@inproceedings
{
    Silveira,

    author         = {Silveira, Ariel Agne da and others},
    title          = {A sound deep embedding of arbitrary normal modal logics in \textsc{coq}},
    year           = {2022},
    isbn           = {9781450397445},
    publisher      = {Association for Computing Machinery},
    doi            = {https://doi.org/10.1145/3561320.3561329},
    booktitle      = {Proceedings of the XXVI Brazilian Symposium on Programming Languages}
}

@article
{
    Tarski,

    author         = {Alfred Tarski},
    title          = {Remarques sur les notions fondamentales de la méthodologie des mathématiques},
    journal        = {Annales de la Société Polonaise de Mathématiques},
    year           = {1928}
}

@book
{
    Troelstra,

    address        = {Cambridge},
    author         = {Anne Sjerp Troelstra and Helmut Schwichtenberg},
    isbn           = {9781139168717},
    publisher      = {Cambridge University Press},
    title          = {Basic proof theory},
    doi            = {https://doi.org/10.1017/CBO9781139168717},
    year           = {2000}
}

@article
{
    Tymoczko,

    author         = {Thomas Tymoczko},
    title          = {The four-color problem and its philosophical significance},
    journal        = {The Journal of Philosophy},
    doi            = {https://doi.org/10.2307/2025976},
    year           = {1979}
}

@book
{
    Velleman,

    address        = {Cambridge},
    author         = {Daniel Jon Velleman},
    publisher      = {Cambridge University Press},
    title          = {How to prove it: a structured approach},
    doi            = {https://doi.org/10.1017/9781108539890},
    year           = {2019}
}

@book
{
    Wilson,

    author         = {Robin Wilson},
    publisher      = {Princeton University Press},
    title          = {Four colors suffice: how the map problem was solved},
    year           = {2021}
}

@book
{
    Zach,

    author         = {Richard Zach and others},
    publisher      = {Open Logic Project},
    title          = {Box and diamonds: an open introcution to modal logic},
    year           = {2024}
}

@article
{
    Glivenko-A,

    author         = {Valerij Ivanovič Glivenko},
    title          = {Sur la logique de monsieur {B}rouwer},
    journal        = {Bulletins de l'Académie Royale de Belgique},
    year           = {1928}
}

@article
{
    Glivenko-B,

    author         = {Valerij Ivanovič Glivenko},
    title          = {Sur quelques points de la logique de monsieur {B}rouwer},
    journal        = {Bulletins de l'Académie Royale de Belgique},
    year           = {1929}
}

@book{Pierce,
  author = {Benjamin Crawford Pierce and others},
  publisher = {Software Foundations},
  title = {Logical foundations},
  year = {2024}
}

@manual{Coq,
  author = {{The \textsc{coq} Development Team}},
  title = {The \textsc{coq} proof assistant reference manual},
  year = {2024}
}

@article
{
    Maraist,

    author         = {John Maraist and others},
    title          = {Call-by-name, call-by-value, call-by-need and the linear lambda calculus},
    journal        = {Theoretical Computer Science},
    doi            = {https://doi.org/10.1016/S0304-3975(98)00358-2},
    year           = {1999}
}

@inproceedings
{
    Wadler,

    author         = {Phillip Wadler},
    title          = {Monads for functional programming},
    year           = {1993},
    isbn           = {978-3-662-02880-3},
    publisher      = {Springer},
    doi            = {https://doi.org/10.1007/978-3-662-02880-3_8},
    booktitle      = {Program Design Calculi}
}