%% This BibTeX bibliography file was created using BibDesk.
%% https://bibdesk.sourceforge.io/

%% Created for Jeremy Dubut at 2023-05-15 08:45:25 +0900 


%% Saved with string encoding Unicode (UTF-8) 



@inproceedings{yamada23,
	author = {Akihisa Yamada and J\'{e}r\'{e}my Dubut},
	booktitle = {Proceedings of the fourteenth conference on Interactive Theorem Proving (ITP'23)},
	date-added = {2023-05-15 08:42:28 +0900},
	date-modified = {2023-05-15 08:45:25 +0900},
	title = {{F}ormalizing {R}esults on {D}irected {S}ets in {I}sabelle/{HOL}},
	year = {2023}}

@article{DubutY21,
	author = {J\'{e}r\'{e}my Dubut and Akihisa Yamada},
	date-added = {2021-01-14 11:30:49 +0900},
	date-modified = {2023-05-15 08:41:50 +0900},
	journal = {Logical Methods in Computer Science},
	number = {1},
	title = {Fixed {P}oints {T}heorems for {N}on-{T}ransitive {R}elations},
	volume = {18},
	year = {2021}}

@inbook{granas03,
	author = {Andrzej Granas and James Dugundji},
	booktitle = {Fixed Point Theory},
	doi = {10.1007/978-0-387-21593-8_2},
	publisher = {Springer},
	series = {Monographs in Mathematics},
	title = {Elementary Fixed Point Theorems},
	year = 2003,
	bdsk-url-1 = {https://doi.org/10.1007/978-0-387-21593-8_2}}

@article{kantorovitch39,
	author = {L. Kantorovitch},
	doi = {doi:10.1007/BF02547750},
	journal = {Acta Math.},
	pages = {63-97},
	title = {The method of successive approximations for functional equations},
	volume = {71},
	year = {1939},
	bdsk-url-1 = {https://doi.org/10.1007/BF02547750}}

@article{jachymski00,
	author = {Jacek Jachymski and Leslaw Gajek and Piotr Pokarowski},
	date-added = {2020-09-11 15:07:37 +0900},
	date-modified = {2020-09-11 15:09:39 +0900},
	journal = {Bulletin of the Australian Mathematical Society},
	number = {2},
	pages = {247--261},
	title = {The {T}arski--{K}antorovitch prinicple and the theory of iterated function systems},
	volume = {61},
	year = {2000}}

@techreport{scott71,
	author = {Dana Scott and Christopher Strachey},
	date-added = {2020-09-09 15:50:30 +0900},
	date-modified = {2020-09-09 15:53:17 +0900},
	institution = {Oxford Programming Research Group},
	number = {PRG-6},
	title = {Toward a mathematical semantics for computer languages},
	type = {Technical Monograph},
	year = {1971}}

@inproceedings{cousot77,
	author = {Patrick Cousot and Radhia Cousot},
	booktitle = {Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL'77)},
	date-added = {2020-09-09 15:42:54 +0900},
	date-modified = {2020-09-09 15:45:38 +0900},
	pages = {238--252},
	publisher = {ACM Press},
	title = {{A}bstract {I}nterpretation: {A} {U}nified {L}attice {M}odel for {S}tatic {A}nalysis of {P}rograms by {C}onstruction or {A}pproximation of {F}ixpoints},
	year = {1977}}

@inproceedings{yamada19,
	author = {Akihisa Yamada and J\'{e}r\'{e}my Dubut},
	booktitle = {Proceedings of the 10th International Conference on Interactive Theorem Proving (ITP 2019)},
	date-added = {2020-08-31 14:39:28 +0900},
	date-modified = {2020-08-31 14:58:11 +0900},
	pages = {30:1--30:16},
	publisher = {Leibniz-Zentrum f{\"u}r Informatik},
	series = {Leibniz International Proceedings in Informatics},
	title = {Complete {N}on-{O}rders and {F}ixed {P}oints},
	volume = {141},
	year = {2019}}

@inproceedings{grall10,
	author = {Herv\'e Grall},
	booktitle = {Fixed Points in Computer Science 2010},
	pages = {41-46},
	title = {Proving fixed points},
	year = 2010}

@article{bourbaki49,
	author = {Nicolas Bourbaki},
	journal = {Archiv der Mathematik},
	number = 6,
	pages = {434--437},
	title = {Sur le th\'eor\`eme de Zorn},
	volume = 2,
	year = 1949}

@misc{pataraia97,
	author = {Dito Pataraia},
	date-added = {2020-08-19 11:52:38 +0900},
	date-modified = {2020-08-19 11:54:15 +0900},
	howpublished = {Presented in the 65th Peripatetic Seminar on Sheaves and Logic, in Aarhus, Denmark},
	title = {A constructive proof of {T}arski's fixed-point theorem for dcpo's},
	year = {1997}}

@article{markowsky76,
	author = {George Markowsky},
	date-added = {2020-08-19 11:47:04 +0900},
	date-modified = {2020-08-19 11:49:10 +0900},
	journal = {Algebra Universalis},
	pages = {53--68},
	title = {Chain{-}complete posets and directed sets with applications},
	volume = {6},
	year = {1976}}

@book{Bergman2015,
	address = {Cham},
	author = {Bergman, George M.},
	doi = {10.1007/978-3-319-11478-1},
	isbn = {978-3-319-11478-1},
	publisher = {Springer International Publishing},
	title = {An Invitation to General Algebra and Universal Constructions},
	year = {2015},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-319-11478-1}}

@book{Schmidt1993,
	address = {Berlin, Heidelberg},
	author = {Schmidt, Gunther and Str{\"o}hlein, Thomas},
	pages = {5--27},
	publisher = {Springer Berlin Heidelberg},
	title = {Relations and Graphs: Discrete Mathematics for Computer Scientists},
	year = {1993}}

@book{gierz03,
	author = {G. Gierz and K. H. Hofmann and K. Keimel and J. D. Lawson and M. W. Mislove and D. S. Scott},
	date-added = {2019-03-29 18:36:56 +0900},
	date-modified = {2019-03-29 18:38:15 +0900},
	doi = {10.1017/CBO9780511542725},
	publisher = {Cambridge University Press},
	title = {Continuous Lattices and Domains},
	year = {2003},
	bdsk-url-1 = {https://doi.org/10.1017/CBO9780511542725}}

@book{abramski94,
	author = {Samson Abramsky and Achim Jung},
	date-added = {2019-03-29 18:27:24 +0900},
	date-modified = {2019-03-29 18:30:21 +0900},
	number = {III},
	publisher = {Oxford University Press},
	series = {Handbook of Logic in Computer Science},
	title = {Domain Theory},
	year = {1994}}

@book{davey02,
	author = {B. A. Davey and H. A. Priestley},
	date-added = {2019-03-29 18:24:39 +0900},
	date-modified = {2019-03-29 18:25:37 +0900},
	doi = {10.1017/CBO9780511809088},
	publisher = {Cambridge University Press},
	title = {Introduction to Lattices and Order},
	year = {2002},
	bdsk-url-1 = {https://doi.org/10.1017/CBO9780511809088}}

@article{mashburn83,
	author = {J. D. Mashburn},
	date-added = {2019-03-27 22:36:00 +0900},
	date-modified = {2019-03-27 22:38:19 +0900},
	journal = {Houston Journal of Mathematics},
	number = {2},
	pages = {231--244},
	title = {The least fixed point property for omega-chain continuous functions},
	volume = {9},
	year = {1983}}

@article{tarski55,
	author = {Alfred Tarski},
	date-added = {2019-03-27 11:16:30 +0900},
	date-modified = {2019-03-27 11:17:45 +0900},
	journal = {Pacific Journal of Mathematics},
	number = {2},
	pages = {285--309},
	title = {A lattice-theoretical fixpoint theorem and its applications},
	volume = {5},
	year = {1955}}

@article{trellis,
	author = {Skala, H.L.},
	doi = {10.1007/BF02944982},
	issue = 1,
	journal = {Algebra Univ.},
	pages = {218--233},
	publisher = {Birkh{\"a}user-Verlag},
	title = {Trellis theory},
	volume = 1,
	year = 1971,
	bdsk-url-1 = {https://doi.org/10.1007/BF02944982}}

@article{SM13,
	author = {Stouti, Abdelkader and Maaden, Abdelhakim},
	doi = {10.4067/S0716-09172013000400008},
	journal = {Proyecciones},
	number = {4},
	pages = {409-418},
	publisher = {Universidad Cat{\'o}lica del Norte, Departamento de Matem{\'a}ticas},
	title = {Fixed points and common fixed points theorems in pseudo-ordered sets},
	volume = {32},
	year = {2013},
	bdsk-url-1 = {https://doi.org/10.4067/S0716-09172013000400008}}

@article{LN83,
	author = {Leutola, K. and Nieminen, J.},
	journal = {Algebra Universalis},
	number = {1},
	pages = {344--354},
	publisher = {Springer},
	title = {Posets and generalized lattices},
	volume = {16},
	year = {1983}}

@article{Bhatta05,
	author = {Bhatta, S. Parameshwara},
	journal = {Czechoslovak Mathematical Journal},
	number = {2},
	pages = {365--369},
	publisher = {Springer},
	title = {Weak chain-completeness and fixed point property for pseudo-ordered sets},
	volume = {55},
	year = {2005}}

@article{BG11,
	author = {Bhatta, S. Parameshwara and George, Shiju},
	date-modified = {2020-09-09 14:15:07 +0900},
	journal = {Algebra and Discrete Mathematics},
	number = {1},
	pages = {17--22},
	publisher = {Луганский национальный университет им. Т. Шевченко},
	title = {Some fixed point theorems for pseudo ordered sets},
	volume = {11},
	year = {2011}}

@article{flyspeck,
	author = {Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat Dat and Harrison, John and Le Truong, Hoang and Kaliszyk, Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat Thang and others},
	doi = {10.1017/fmp.2017.1},
	journal = {Forum of Mathematics, Pi},
	pages = {e2},
	publisher = {Cambridge University Press},
	title = {A formal proof of the {K}epler conjecture},
	volume = {5},
	year = {2017},
	bdsk-url-1 = {https://doi.org/10.1017/fmp.2017.1}}

@article{4color,
	author = {Gonthier, Georges},
	journal = {Notices of the AMS},
	number = {11},
	pages = {1382--1393},
	title = {Formal proof -- the four-color theorem},
	volume = {55},
	year = {2008}}

@inproceedings{sel4,
	author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Wiwood, Simon},
	booktitle = {Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP 2009)},
	doi = {10.1145/1629575.1629596},
	organization = {ACM},
	pages = {207--220},
	title = {se{L}4: Formal verification of an {OS} kernel},
	year = {2009},
	bdsk-url-1 = {https://doi.org/10.1145/1629575.1629596}}

@inproceedings{isabelle/jedit,
	author = {Wenzel, Makarius},
	booktitle = {Proceedings of the 5th Conferences on Intelligent Computer Mathematics (CICM 2012)},
	doi = {10.1007/978-3-642-31374-5_38},
	pages = {468--471},
	publisher = {Springer Berlin Heidelberg},
	series = {LNCS},
	title = {{I}sabelle/j{E}dit -- a Prover {IDE} within the {PIDE} framework},
	volume = 7362,
	year = {2012},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-31374-5_38}}

@inproceedings{quickcheck,
	acmid = {1030056},
	author = {Berghofer, Stefan and Nipkow, Tobias},
	booktitle = {Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004)},
	doi = {10.1109/SEFM.2004.36},
	numpages = {10},
	opaddress = {Washington, DC, USA},
	opisbn = {0-7695-2222-X},
	pages = {230--239},
	publisher = {IEEE Computer Society},
	title = {Random Testing in {I}sabelle/{HOL}},
	year = {2004},
	bdsk-url-1 = {https://doi.org/10.1109/SEFM.2004.36}}

@inproceedings{nitpick,
	author = {Blanchette, Jasmin Christian and Nipkow, Tobias},
	booktitle = {Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010)},
	doi = {10.1007/978-3-642-14052-5_11},
	editor = {Kaufmann, Matt and Paulson, Lawrence C.},
	opaddress = {Berlin, Heidelberg},
	pages = {131--146},
	publisher = {Springer Berlin Heidelberg},
	series = {LNCS},
	title = {Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder},
	volume = 6172,
	year = {2010},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-14052-5_11}}

@inproceedings{codegen,
	author = {Haftmann, Florian and Nipkow, Tobias},
	booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends},
	editor = {Klaus Schneider and Jens Brandt},
	opnumber = {364/07},
	pages = {128--143},
	publisher = {Department of Computer Science, University of Kaiserslautern},
	title = {A code generator framework for {I}sabelle/{HOL}},
	year = {2007}}

@inproceedings{locale,
	author = {Ballarin, Clemens},
	booktitle = {Proceedings of the 5th International Conference on Mathematical Knowledge Management (MKM 2006)},
	doi = {10.1007/11812289_4},
	editor = {Borwein, Jonathan M. and Farmer, William M.},
	opaddress = {Berlin, Heidelberg},
	opisbn = {978-3-540-37106-9},
	pages = {31--43},
	publisher = {Springer Berlin Heidelberg},
	series = {LNCS},
	title = {Interpretation of Locales in {I}sabelle: Theories and Proof Contexts},
	volume = 4108,
	year = {2006},
	bdsk-url-1 = {https://doi.org/10.1007/11812289_4}}

@inproceedings{Kammuller00,
	author = {Kamm{\"u}ller, Florian},
	booktitle = {Proceedings of the 17th International Conference on Automated Deduction (CADE-17)},
	doi = {10.1007/10721959_7},
	editor = {McAllester, David},
	opaddress = {Berlin, Heidelberg},
	pages = {99--114},
	publisher = {Springer Berlin Heidelberg},
	series = {LNCS},
	title = {Modular Reasoning in {I}sabelle},
	volume = 1831,
	year = {2000},
	bdsk-url-1 = {https://doi.org/10.1007/10721959_7}}

@inproceedings{isafor,
	author = {Thiemann, Ren{\'e} and Sternagel, Christian},
	booktitle = {International Conference on Theorem Proving in Higher Order Logics},
	organization = {Springer},
	pages = {452--468},
	title = {Certification of termination proofs using {CeTA}},
	year = {2009}}

@book{Isabelle,
	author = {T.~Nipkow and L.C.~Paulson and M.~Wenzel},
	doi = {10.1007/3-540-45949-9},
	publisher = {Springer},
	series = {LNCS},
	title = {{Isabelle/HOL} -- A Proof Assistant for Higher-Order Logic},
	volume = 2283,
	year = 2002,
	bdsk-url-1 = {https://doi.org/10.1007/3-540-45949-9}}

@inproceedings{hol4,
	author = {Slind, Konrad and Norrish, Michael},
	booktitle = {International Conference on Theorem Proving in Higher Order Logics},
	organization = {Springer},
	pages = {28--32},
	title = {A brief overview of {HOL4}},
	year = {2008}}

@inproceedings{hol-light,
	author = {Harrison, John},
	booktitle = {International Conference on Theorem Proving in Higher Order Logics},
	organization = {Springer},
	pages = {60--66},
	title = {{HOL} light: An overview},
	year = {2009}}

@inproceedings{agda,
	author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
	booktitle = {International Conference on Theorem Proving in Higher Order Logics},
	organization = {Springer},
	pages = {73--78},
	title = {A brief overview of {A}gda -- a functional language with dependent types},
	year = {2009}}

@book{coq,
	author = {Chlipala, Adam},
	publisher = {MIT Press},
	title = {Certified programming with dependent types: a pragmatic introduction to the {C}oq proof assistant},
	year = {2013}}

@inproceedings{compcert,
	author = {Krebbers, Robbert and Leroy, Xavier and Wiedijk, Freek},
	booktitle = {International Conference on Interactive Theorem Proving},
	organization = {Springer},
	pages = {543--548},
	title = {Formal {C} semantics: {C}omp{C}ert and the {C} standard},
	year = {2014}}

@inproceedings{sledgehammer,
	author = {B{\"o}hme, Sascha and Nipkow, Tobias},
	booktitle = {Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010)},
	doi = {10.1007/978-3-642-14203-1_9},
	pages = {107--121},
	publisher = {Springer Berlin Heidelberg},
	series = {LNCS},
	title = {Sledgehammer: Judgement Day},
	volume = 6173,
	year = {2010},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-14203-1_9}}
