@jonaprieto Blog

List of references


Jonathan Prieto-Cubides
University of Bergen
Latest change:
New version published. Clean and simpler build.
Latest commit b2dabf7 on 24 May 2019

List of references

  1. Buurlage, J.-willem. (2018). Categories and Haskell.
  2. Mario Román. (2018). Category Theory and Lambda Calculus (PhD thesis).
  3. Escardó, M. H. (2018). A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom, 1–9. Retrieved from http://arxiv.org/abs/1803.02294
  4. Colin de Verdière, É., Magnard, T., & Mohar, B. (2018). Embedding graphs into two-dimensional simplicial complexes, (SoCG 2018). https://doi.org/10.4230/LIPIcs.SoCG.2018.27
  5. Bradley, T.-D. (2018). What is Applied Category Theory? Retrieved from http://arxiv.org/abs/1809.05923
  6. Speight, S. (2018). Impredicative Encodings of Inductive Types in Homotopy Type Theory, (January).
  7. Abel, A., Devriese, D., Cockx, J., Wadler, P., & Timany, A. (2018). Leibniz Equality is Isomorphic to Martin-Löf Identity , Parametrically, (May). Retrieved from https://jesper.sikanda.be/files/leibniz-equality.pdf
  8. Zalakain, U. (2018). Evidence-providing problem solvers in Agda, 2017–2018.
  9. Brunerie, G., Hou (Favonia), K.-B., Cavallo, E., Finster, E., Cockx, J., Sattler, C., … Others. (2018). Homotopy Type Theory in Agda. Retrieved from https://github.com/HoTT/HoTT-Agda
  10. Doorn, F. V., Avigad, J., & Shulman, M. (2018). On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, (May).
  11. Paleo, B. W. (2018). Encyclopedia of Proof Systems.
  12. Grayson, D. R. (2017). An Introduction to Univalent Foundations for Mathematicians. Retrieved from http://arxiv.org/abs/1711.01477
  13. Prieto-Cubides, J. (2017). A Collection of Propositional Problems in TPTP Format. https://doi.org/10.5281/ZENODO.817997
  14. Prieto-Cubides, J. (2017). A Translator Tool for Metis Proofs in Haskell. https://doi.org/10.5281/zenodo.437196
  15. Mokhov, A., Andrey, Mokhov, & Andrey. (2017). Algebraic graphs with class (functional pearl). In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell - Haskell 2017 (Vol. 52, pp. 2–13). New York, New York, USA: ACM Press. https://doi.org/10.1145/3122955.3122956
  16. Agudelo-Agudelo, J. C. (2017). Translating Non-classical Logics into Classical Logic by Using Hidden Variables. Logica Universalis, 11(2), 205–224. https://doi.org/10.1007/s11787-017-0168-1
  17. Bauer, A. (2017). Five stages of accepting constructive mathematics. Bulletin of the American Mathematical Society, 54(3), 481–498. https://doi.org/10.1090/bull/1556
  18. Norrish, M., & Slind, K. (2017). The HOL system description. Retrieved from https://goo.gl/iG8b9M
  19. Cockx, J. (2017). Dependent pattern matching and proof-relevant unification, (June).
  20. Lammich, P., & Sefidgar, S. R. (2017). Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. Journal of Automated Reasoning. https://doi.org/10.1007/s10817-017-9442-4
  21. Prieto-Cubides, J. (2017). Reconstructing Propositional Proofs in Type Theory (PhD thesis). Universidad EAFIT. Retrieved from https://goo.gl/5whnJd
  22. Chlipala, A. (2017). Certified Programming with Dependent Types. MIT Press. Retrieved from http://adam.chlipala.net/cpdt/cpdt.pdf
  23. Ekici, B., Mebsout, A., Tinelli, C., Keller, C., & Katz, G. (2017). SMTCoq: A plug-in for integrating SMT solvers into Coq. Stanford.edu. Retrieved from https://goo.gl/3JKsyc
  24. Rahman, M. S. (2017). Basic Graph Theory. https://doi.org/10.1007/978-3-319-49475-3
  25. Zeng, A., Li, T., Luo, C., & Hu, J. (2017). Dynamical updating fuzzy rough approximations for hybrid data under the variation of attribute values. Proceedings - International Conference on Machine Learning and Cybernetics, 1, 157–162. https://doi.org/10.1109/ICMLC.2015.7340915
  26. Lonsing, F., & Egly, U. (2017). DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. In International Conference on Automated Deduction. Gotenburg: Springer. Retrieved from https://arxiv.org/pdf/1702.08256.pdf
  27. Diestel, R. (2017). Graph Theory (Vol. 173). https://doi.org/10.1007/978-3-662-53622-3
  28. Prieto-Cubides, J. (2017). A Library for Classical Propositional Logic in Agda. https://doi.org/10.5281/zenodo.398852
  29. Laaksonen, A. (2017). Competitive Programmer’s Handbook.
  30. Bergsten, E. (2017). Methods for using Agda to prove Safety and Liveness for Concurrent Programs, (June).
  31. Stanford Encyclopedia of Philosophy. (2017). Type Theory, (September), 1–22. https://doi.org/10.1111/1467-9973.00225
  32. Prieto-Cubides, J. (2017). Metis Prover Reasoning for Propositional Logic in Agda. https://doi.org/10.5281/zenodo.398862
  33. Mokhov, A. (2017). Algebraic graphs with class (functional pearl). Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell - Haskell 2017, 2–13. https://doi.org/10.1145/3122955.3122956
  34. Erwing, M. (2017). Inductive Graphs and Functional Graph Algorithms.
  35. Prieto-Cubides, J. (2017). OnlineATPs: A command-line tool client for the TPTP World. https://doi.org/10.5281/zenodo.398851
  36. Colin de Verdière, É. (2017). Computational Topology of Graphs on Surfaces.
  37. Cockx, J., Devriese, D., & Piessens, F. (2016). Eliminating dependent pattern matching without K. Journal of Functional Programming, 1–40. https://doi.org/10.1017/S0956796816000174
  38. Brunerie, G. (2016). On the homotopy groups of spheres in homotopy type theory. Retrieved from http://arxiv.org/abs/1606.05916
  39. Blanchette, J., Böhme, S., Fleury, M., Smolka, S. J., & Steckermeier, A. (2016). Semi-intelligible Isar Proofs from Machine-Generated Proofs. Journal of Automated Reasoning, 56(2), 155–200. https://doi.org/10.1007/s10817-015-9335-3
  40. Mycroft, A. (2016). Introduction Hoare Logic and Model Checking.
  41. Clark, P. G., Gao, C., & Grzymala-busse, J. W. (2016). Rule Set Complexity for Incomplete Data Sets with Many Attribute-Concept Values and Do Not Care Conditions, 9920, 65–74. https://doi.org/10.1007/978-3-319-47160-0
  42. Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2016). Cubical Type Theory: a constructive interpretation of the univalence axiom, 1–34. https://doi.org/10.4230/LIPIcs.TYPES.2015.5
  43. Hall/CRC, & Chapman. (2016). Handbook of Graph Theory , Combinatorial Optimization , and Algorithms Series Editor : Sartaj Sahni (p. 1226).
  44. Sicard-Ramírez, A., & Ospina-Giraldo, J.-F. (2016). First-Order Proof Reconstruction (Research Proposal). Medellín, Colombia: Universidad EAFIT.
  45. Nipkow, T., & Klein, G. (2016). Concrete Semantics (pp. 1–2). https://doi.org/10.1007/978-3-319-10542-0
  46. Färber, M., & Kaliszyk, C. (2016). No choice: Reconstruction of first-order ATP proofs without skolem functions. CEUR Workshop Proceedings, 1635(Paar), 24–31. Retrieved from https://goo.gl/V9dsoH
  47. Zhang, Y., Li, T., Luo, C., Zhang, J., & Chen, H. (2016). Incremental updating of rough approximations in interval-valued information systems under attribute generalization. Information Sciences, 373, 1339–1351. https://doi.org/10.1016/j.ins.2016.09.018
  48. van der Weide, N. (2016). Higher Inductive Types. RADBOUD UNIVERSITY. Retrieved from http://arxiv.org/abs/1803.07032%0Ahttps://arxiv.org/abs/1803.07032
  49. Erb, C., Carter, N., Mcmichael, W., Samuel, S., & Krueger, D. (2016). Forall X.
  50. Borradaile, G., Chambers, E. W., Fox, K., & Nayyeri, A. (2016). Minimum cycle and homology bases of surface embedded graphs. https://doi.org/10.4230/LIPIcs.SoCG.2016.23
  51. Kanso, K., & Setzer, A. (2016). A Light-weight Integration Of Automated And Interactive Theorem Proving. Mathematical Structures in Computer Science, 26(1), 129–153. https://doi.org/10.1017/S0960129514000140
  52. Wadler, P. (2015). Propositions As Types. Commun. ACM, 58(12), 75–84. https://doi.org/10.1145/2699407
  53. Luo, C., Li, T., Chen, H., & Lu, L. (2015). Fast algorithms for computing rough approximations in set-valued decision systems while updating criteria values. Information Sciences, 299, 221–242. https://doi.org/10.1016/j.ins.2014.12.029
  54. Welzl, E. (2015). Geometry: Combinatorics & Algorithms Lecture Notes HS 2014.
  55. Sultana, N., Benzmüller, C., & Paulson, L. C. (2015). Proofs and Reconstructions. In C. Lutz & S. Ranise (Eds.), Frontiers of Combining Systems: 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings (pp. 256–271). Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-24246-0_16
  56. Leary, C. C., & Kristiansen, L. (2015). A Friendly Introduction to Mathematical Logic.
  57. Cai, L., Kaposi, A., & Altenkirch, T. (2015). Formalising the Completeness Theorem of Classical Propositional Logic in Agda. Retrieved from https://akaposi.github.io/proplogic.pdf
  58. Färber, M., & Kaliszyk, C. (2015). Metis-based Paramodulation Tactic for HOL Light. In GCAI 2015. Global Conference on Artificial Intelligence Metis-based (Vol. 36, pp. 127–136).
  59. Mynhardt, C. M. K., Bommel, C. M. V., & Vw, C. (2015). Triangle Decompositions of Planar Graphs, 1–14.
  60. Gómez-Londoño, A. (2015). Proof Reconstruction: Parsing Proofs. EAFIT University. Retrieved from http://repository.eafit.edu.co/handle/10784/5484
  61. Rojas, R. (2015). A Tutorial Introduction to the Lambda Calculus, 1–9. https://doi.org/10.1006/anbe.1999.1219
  62. Team, T. C. D. (2015). The Coq Proof Assistant. Reference Manual. Retrieved from https://coq.inria.fr/distrib/current/files/Reference-Manual.pdf
  63. Miraldo, V. C. (2015). Proof by Rewriting in Agda (PhD thesis).
  64. Sicard-Ramírez, A., Bove, A., & Dybjer, P. (2015). Reasoning about Functional Programs by Combining Interactive and Automatic Proofs (PhD thesis). Universidad de la Rep{ú}blica. Retrieved from https://www.colibri.udelar.edu.uy/handle/123456789/4715
  65. Liu, D., Liang, D., & Wang, C. (2015). A novel three-way decision model based on incomplete information system. Knowledge-Based Systems, 91(July), 32–45. https://doi.org/10.1016/j.knosys.2015.07.036
  66. Beringer, L., Petcher, A., Ye, K. Q., & Appel, A. W. (2015). Verified correctness and security of OpenSSL HMAC. Usenix Sec. https://doi.org/10.1145/3133956.3133974
  67. Licata, D. R., & Brunerie, G. (2015). A cubical approach to synthetic homotopy theory. Proceedings - Symposium on Logic in Computer Science, 2015-July, 92–103. https://doi.org/10.1109/LICS.2015.19
  68. Team, T. A. D. (2015). Agda 2.4.2.3. Retrieved from http://wiki.portal.chalmers.se/agda/pmwiki.php
  69. Zhang, J., Wong, J. S., Pan, Y., & Li, T. (2015). A parallel matrix-based method for computing approximations in incomplete information systems. IEEE Transactions on Knowledge and Data Engineering, 27(2), 326–339. https://doi.org/10.1109/TKDE.2014.2330821
  70. Noschinski, L. (2015). Formalizing Graph Theory and Planarity Certificates.
  71. Mokhov, A., & Khomenko, V. (2014). Algebra of Parameterised Graphs. ACM Transactions on Embedded Computing Systems, 13(4s), 1–22. https://doi.org/10.1145/2627351
  72. Luo, C., & Li, T. (2014). Incremental three-way decisions with incomplete information. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8536 LNAI, 128–135. https://doi.org/10.1007/978-3-319-08644-6_13
  73. Colin de Verdière, É., & de Mesmay, A. (2014). Testing Graph Isotopy on Surfaces. Discrete and Computational Geometry, 51(1), 171–206. https://doi.org/10.1007/s00454-013-9555-4
  74. Klieber, W. (2014). Formal Verification Using Quantified Boolean Formulas (QBF) (PhD thesis). Carnegie Mellon University. Retrieved from https://goo.gl/Mokhmz
  75. Spivak, D. (2014). Category theory for the sciences. arXiv preprint arXiv:1302.6946 (p. 495). MIT Press. https://doi.org/10.1017/CBO9781107415324.004
  76. Fleury, M., & Blanchette, J. (2014). Translation of Proofs Provided by External Provers More Automatic Prover Support for Isabelle: Two Higher-Order Provers and a SMT Solver (pp. 2–0). Techniche Universität München. Retrieved from https://goo.gl/Kw6wWR
  77. Isaza, J. P. V. (2014). Category Theory Applied to Functional Programming (PhD thesis). Eafit.Edu.Co. Universidad EAFIT. Retrieved from http://www1.eafit.edu.co/asicard/pubs/cain-screen.pdf
  78. Avigad, J., & Harrison, J. (2014). Formally Verified Mathematics. Communications of the ACM, 57(4), 66–75. Retrieved from https://goo.gl/nkhtrq
  79. Kahle, R. (2014). What is a Proof? Axiomathes, 79–91. https://doi.org/10.1007/s10516-014-9252-9
  80. Wadler, P. (2014). Propositions as sessions, 24(January), 384–418. https://doi.org/10.1017/S095679681400001X
  81. Yorgey, B. A. (2014). Combinatorial Species And Labelled Structures (PhD thesis). Retrieved from https://books.google.com/books?id=83odtWY4eogC&pgis=1
  82. Milewski, B. (2014). Category Theory for Programmers. Retrieved from https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
  83. Blanchette, J., Böhme, S., & Paulson, L. C. (2013). Extending Sledgehammer with SMT Solvers. Journal of Automated Reasoning, 51(1), 109–128. https://doi.org/10.1007/s10817-013-9278-5
  84. Marlow, S. (2013). Parallel and Concurrent Programming in Haskell: Techniques for Multicore and Multithreaded Programming. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7241 LNCS, p. 322). Retrieved from http://chimera.labs.oreilly.com/books/1230000000929
  85. Geuvers, H. (2013). Pure Type Systems, (November), 5–7.
  86. Raynal, M. (2013). Concurrent programming: Algorithms, principles, and foundations. Concurrent Programming: Algorithms, Principles, and Foundations (Vol. 9783642320, pp. 1–515). https://doi.org/10.1007/978-3-642-32027-9
  87. Carlstrõm, J. (2013). Logic, 2008.
  88. Licata, D. R., & Shulman, M. (2013). Calculating the fundamental group of the circle in homotopy type theory. Proceedings - Symposium on Logic in Computer Science, 223–232. https://doi.org/10.1109/LICS.2013.28
  89. Salomaa, A. (2013). Public-Key Cryptography (Texts in Theoretical Computer Science. An EATCS Series) (pp. 1–288). https://doi.org/10.1007/978-3-642-16533-7
  90. Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. Retrieved from http://saunders.phil.cmu.edu/book/hott-online.pdf
  91. SIAM. (2013). SIAM Style Manual (p. 122).
  92. Keller, C. (2013). A Matter of Trust: Skeptical Communication Between Coq and External Provers (PhD thesis). Retrieved from https://hal.archives-ouvertes.fr/pastel-00838322/
  93. Burel, G. (2013). A Shallow Embedding of Resolution and Superposition Proofs into the λ\Pi -Calculus. In Third International Workshop on Proof Exchange for Theorem Proving, (pp. 1–15).
  94. Stump, A., Oe, D., Reynolds, A., Hadarean, L., & Tinelli, C. (2013). SMT proof checking using a logical framework. Formal Methods in System Design, 42(1), 91–118. https://doi.org/10.1007/s10703-012-0163-3
  95. Van Der Walt, P., & Swierstra, W. (2013). Engineering proof by reflection in Agda. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8241 LNCS, 157–173. https://doi.org/10.1007/978-3-642-41582-1_10
  96. Kaliszyk, C., & Urban, J. (2013). PRocH: Proof Reconstruction for HOL Light. In M. P. Bonacina (Ed.), Automated Deduction – CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings (pp. 267–274). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_18
  97. Micinski, K. (2012). Functional Programming with Bananas , Lenses , Envelopes and Barbed Wire, 2012.
  98. Baur, M. (2012). Combinatorial Concepts and Algorithms for Drawing Planar Graphs.
  99. Bove, A., Dybjer, P., & Sicard-Ramírez, A. (2012). Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7213 LNCS, pp. 104–118). Springer. https://doi.org/10.1007/978-3-642-28729-9_7
  100. Awodey, S. (2012). Type theory and homotopy. Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of per Martin-Lof, 183–201. https://doi.org/10.1007/978-94-007-4435-6_9
  101. Kanso, K. (2012). Agda as a Platform for the Development of Verified Railway Interlocking Systems. Retrieved from http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.310.1502
  102. Kunen, K. (2012). The Foundations of Mathematics.
  103. Brown, C. E. (2012). Satallax: An automatic higher-order prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7364 LNAI, pp. 111–117). https://doi.org/10.1007/978-3-642-31365-3_11
  104. Humberstone, L. (2011). The Connectives. MIT Press.
  105. Böhme, S., & Weber, T. (2011). Designing Proof Formats: A User’s Perspective - Experience Report. In First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011. Retrieved from http://hal.inria.fr/hal-00677244
  106. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., & Werner, B. (2011). A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In Certified Programs and Proofs: First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings (pp. 135–150). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-25379-9_12
  107. Harrison, J. (2011). Software and Systems Safety - Specification and Verification. In M. Broy, C. Leuxner, & T. Hoare (Eds.) (pp. 103–157). IOS Press.
  108. Barrett, C., Conway, C. L., Deters, M., Hadarean, L., Jovanović, D., King, T., … Tinelli, C. (2011). CVC4. In G. Gopalakrishnan & S. Qadeer (Eds.), Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (pp. 171–177). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_14
  109. Foster, S., & Struth, G. (2011). Integrating an Automated Theorem Prover into Agda. In NASA Formal Methods: Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings (pp. 116–130). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_10
  110. Hanks, P. W. (2011). Structured propositions as types. Mind, 120(477), 11–52. https://doi.org/10.1093/mind/fzr011
  111. Awodey, S. (2010). Category Theory.
  112. Armand, M., Grégoire, B., Spiwack, A., & Théry, L. (2010). Extending Coq with imperative features and its application to SAT verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6172 LNCS, pp. 83–98). https://doi.org/10.1007/978-3-642-14052-5_8
  113. Avigad, J. (2010). Understanding, formal verification, and the philosophy of mathematics. Journal of Indian Council of Philosophical \Ldots, 1–27. Retrieved from http://www.andrew.cmu.edu/user/avigad/Papers/understanding2.pdf
  114. Böhme, S., & Weber, T. (2010). Fast LCF-Style Proof Reconstruction for Z3. In M. Kaufmann & L. C. Paulson (Eds.), Interactive Theorem Proving: First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (pp. 179–194). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_14
  115. Kanso, K. (2010). Formal Verification of Ladder Logic (PhD thesis). Swansea University. Retrieved from https://goo.gl/1Mj3oa
  116. van Benthem, J. (2010). Modal Logic for Open Minds. Chart, (199), 1–390. Retrieved from http://fenrong.net/teaching/mljvb.pdf
  117. Paulson, L. C., & Blanchette, J. (2010). Three Years Of Experience with Sledgehammer, A Practical Link Between Automatic And Interactive Theorem Provers. In PAAR@ IJCAR (pp. 1–10).
  118. Avigad, J. (2010). Understanding Proofs. The Philosophy of Mathematical Practice, (May 2005). https://doi.org/10.1093/acprof:oso/9780199296453.003.0013
  119. Sutcliffe, G. (2009). The TPTP Problem Library and Associated Infrastructure. Journal of Automated Reasoning, 43(4), 337. https://doi.org/10.1007/s10817-009-9143-8
  120. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., & Wischnewski, P. (2009). SPASS version 3.5. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5663 LNAI, pp. 140–145). https://doi.org/10.1007/978-3-642-02959-2_10
  121. Norell, U. (2009). Dependently typed programming in agda. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5832 LNCS(Agda 2), 230–266. https://doi.org/10.1007/978-3-642-04652-0_5
  122. of Philosophy, S. E. (2009). Second-order and Higher-order Logic.
  123. Klein, G., Norrish, M., Sewell, T., Tuch, H., Winwood, S., Elphinstone, K., … Kolanski, R. (2009). seL4. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles - SOSP ’09 (p. 207). New York, New York, USA: ACM Press. https://doi.org/10.1145/1629575.1629596
  124. Grädel, E. (2009). Complexity Theory.
  125. Weber, T., & Amjad, H. (2009). Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic, 7(1), 26–40. https://doi.org/10.1016/j.jal.2007.07.003
  126. Bouton, T., de Oliveira, D., Déharbe, D., & Fontaine, P. (2009). veriT: An Open, Trustable and Efficient SMT-Solver. In Automated Deduction – CADE-22: 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings (pp. 151–156). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_12
  127. Dufourd, J. F. (2009). An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps. Journal of Automated Reasoning, 43(1), 19–51. https://doi.org/10.1007/s10817-009-9117-x
  128. Bove, A., & Dybjer, P. (2009). Dependent types at work. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5520 LNCS, 57–99. https://doi.org/10.1007/978-3-642-03153-3_2
  129. Harrison, J. (2009). Formalizing an analytic proof of the {P}rime {N}umber {T}heorem (Dedicated to {M}ike {G}ordon on the occasion of his 60th birthday). Journal of Automated Reasoning, 43, 243–261.
  130. Stump, A., & Oe, D. (2008). Towards an SMT proof format. In Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning - SMT ’08/BPR ’08 (p. 27). New York, New York, USA: ACM Press. https://doi.org/10.1145/1512464.1512470
  131. Narayan, G., Gopinath, K., & Sridhar, V. (2008). Structure and interpretation of computer programs. Proceedings - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, 73–80. https://doi.org/10.1109/TASE.2008.40
  132. Steinberg, R. (2008). Perfect Phrases for the TOEFL Speaking and Writing Sections (p. 224). https://doi.org/10.1007/s13398-014-0173-7.2
  133. Benzmüller, C., Paulson, L. C., Theiss, F., & Fietzke, A. (2008). LEO-II - A cooperative automatic theorem prover for classical higher-order logic (system description). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 162–170). https://doi.org/10.1007/978-3-540-71070-7_14
  134. Gonthier, G. (2008). Formal proof–the four-color theorem. Notices of the AMS, 55(11), 1382–1393. https://doi.org/10.1.1.141.714
  135. Ge, Y., & Barrett, C. (2008). Proof Translation and SMT-LIB Benchmark Certification: A Preliminary Report. Proceedings of the 6\^{Th} International Workshop on Satisfiability Modulo Theories (SMT ’08), (0551645), 1–11. Retrieved from https://goo.gl/HwUUUK
  136. De Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT Solver. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4963 LNCS, pp. 337–340). https://doi.org/10.1007/978-3-540-78800-3_24
  137. Otten, J. (2008). leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions). In Automated Reasoning (pp. 283–291). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_23
  138. Levin, O. (2008). Discrete Mathematics An Open Introduction. Animal Genetics (Vol. 39, pp. 561–563).
  139. Seldin, J. P. (2008). On the relation between Church-style typing and Curry-style typing ∗, 1–24.
  140. Baier, C., & Katoen, J.-P. (2008). Principles Of Model Checking. MIT Press (Vol. 950, pp. I–XVII, 1–975). https://doi.org/10.1093/comjnl/bxp025
  141. Hurlin, C., Chaieb, A., Fontaine, P., Merz, S., & Weber, T. (2007). Practical Proof Reconstruction for First-Order Logic and Set-Theoretical Constructions. In L. Dixon & M. Johansson (Eds.), Proceedings of the Isabelle Workshop 2007 (pp. 2–13). Bremen, Germany.
  142. Sutcliffe, G. (2007). TPTP, TSTP, CASC, etc. In V. Diekert, M. Volkov, & A. Voronkov (Eds.), Proceedings of the 2nd International Computer Science Symposium in Russia (pp. 7–23). Springer-Verlag.
  143. Hofstadter, D. (2007). Godel, Escher, Bach. Journal of Experimental Psychology: General, 136(1), 23–42.
  144. Kimura, D. (2007). Call-by-value is dual to call-by-name, extended. Programming Languages and Systems, Proceedings, 4807(April 2005), 415–430.
  145. Harrison, J. (2007). A short survey of automated reasoning. In H. Anai, K. Horimoto, & T. Kutsia (Eds.), Proceedings of the Second International Conference on Algebraic Biology, AB 2007 (Vol. 4545, pp. 334–349). Castle of Hagenberg, Austria: Springer-Verlag.
  146. Paulson, L. C., & Susanto, K. W. (2007). Source-level Proof Reconstruction For Interactive Theorem Proving. In TPHOLs (Vol. 4732, pp. 232–245). Springer. https://doi.org/https://doi.org/10.1007/978-3-540-74591-4_18
  147. Castillo, C. I. (2006). Topologia Algebraica, 521.
  148. Dasgupta, S., & Papadimitriou, C. H. (2006). Algorithms. Book.
  149. Weber, T. (2006). Integrating a SAT solver with an LCF-style theorem prover. In Electronic Notes in Theoretical Computer Science (Vol. 144, pp. 67–78). https://doi.org/10.1016/j.entcs.2005.12.007
  150. Fontaine, P., Marion, J. Y., Merz, S., Nieto, L. P., & Tiu, A. (2006). Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3920 LNCS, 167–181. https://doi.org/10.1007/11691372_11
  151. Sutcliffe, G., Schulz, S., Claessen, K., & Van Gelder, A. (2006). Using the TPTP Language for Writing Derivations and Finite Interpretations. In U. Furbach & N. Shankar (Eds.), International Joint Conference on Automated Reasoning (IJCAR 2006) (Vol. 4130, pp. 67–81). Springer.
  152. Nieuwenhuis, R., Nieuwenhuis, R., Oliveras, A., Oliveras, A., Tinelli, C., & Tinelli, C. (2006). Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T). J. Acm, 53(6), 937–977. https://doi.org/10.1145/1217856.1217859
  153. Meng, J., Quigley, C., & Paulson, L. C. (2006). Automation for Interactive Proof: First Prototype. Information and Computation, 204(10), 1575–1596.
  154. Jackson, D. (2006). Software Abstractions. MIT Press (Vol. 19, p. 253).
  155. Bove, A., & Capretta, V. (2005). Recursive Functions with Higher Order Domains (pp. 116–130). Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_10
  156. Hinze, R. (2005). Church numerals, twice! Journal of Functional Programming, 15(1), 1–13. https://doi.org/10.1017/S0956796804005313
  157. Mehta, D. P., & Sahni, S. (2005). Handbook of DATA STRUCTURES and APPLICATIONS. New York.
  158. Blackburn, P., & Benthem, J. V. (2005). Modal Logic: A Semantic Perspective, 1–50. Retrieved from papers2://publication/uuid/CC567B68-4635-4E4C-A795-06E2E0B6C800
  159. Bauer, G. J. (2005). Formalizing Plane Graph Theory – Towards a Formalized Proof of the Kepler Conjecture (PhD thesis). Retrieved from https://goo.gl/jxNXcV
  160. Mossakowski, T., Goguen, J., Diaconescu, R., & Tarlecki, A. (2005). What is a Logic? Logica Universalis, 113–133. Retrieved from https://goo.gl/i3CdWX
  161. Bertot, Y., & Castéran, P. (2004). Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer. https://doi.org/10.1007/978-3-662-07964-5
  162. Sutcliffe, G., Zimmer, J., & Schulz, S. (2004). TSTP data-exchange formats for automated theorem proving tools. Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, 112, 201–215.
  163. Tucker, A. B. (2004). Computer Science Handbook.
  164. McBride, C. (2004). Dependently Typed Functional Programs and their Proofs. Retrieved from http://hdl.handle.net/1842/374
  165. Eén, N., & Sörensson, N. (2004). An Extensible SAT-solver (pp. 502–518). Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_37
  166. Setzer, A. (2004). Proof Theory of Martin-Löf Type Theory – An Overview The Notion of Proof-Theoretic Strength, 1–35.
  167. Strecker, G. E. (2004). Concrete Categories: The Joy of Cats.
  168. of Philosophy, S. E. (2003). Constructive Mathematics. Www.Plato.Stanford.Edu/Entries/Qualia.
  169. Hurd, J. (2003). First-order Proof Tactics In Higher-order Logic Theorem Provers. Design and Application of Strategies/Tactics in Higher Order Logics, Number NASA/CP-2003-212448 in NASA Technical Reports, 56–68. Retrieved from http://www.gilith.com/research/papers
  170. Wadler, P. (2003). Call-by-Value is Dual to Call-by-Name, (1935).
  171. Jordan, R. R. (2003). Academic writing course : study skills in English.
  172. Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-order Logic (Vol. 2283). Springer Science & Business Media.
  173. Schulz, S. (2002). E – A Brainiac Theorem Prover. Journal of AI Communications, 15(2/3), 111–126.
  174. Bauer, G., & Nipkow, T. (2002). The 5 Colour Theorem in Isabelle/Isar. In Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings (pp. 67–82). https://doi.org/10.1007/3-540-45685-6_6
  175. Carreño, V., Muñoz, C. A., & Tahar, S. (Eds.). (2002). Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings (Vol. 2410). Springer. https://doi.org/10.1007/3-540-45685-6
  176. Bezem, M., Hendriks, D., & De Nivelle, H. (2002). Automated proof construction in type theory using resolution. Journal of Automated Reasoning, 29(3-4), 253–275. https://doi.org/10.1023/A:1021939521172
  177. Abel, A., & Altenkirch, T. (2002). A Predicative Analysis of Structural Recursion. Journal of Functional Programming, 12(01), 1–41. https://doi.org/10.1017/S0956796801004191
  178. Bove, A. (2002). General recursion in type theory. Doktorsavhandlingar Vid Chalmers Tekniska Hogskola, (1889), 39–58. https://doi.org/10.1017/S0960129505004822
  179. Stefanowski, J., & Tsoukiàs, A. (2001). Incomplete information tables and rough classification. Computational Intelligence, 17(3), 545–566. https://doi.org/10.1111/0824-7935.00162
  180. Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001). Chaff: engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC 2001) (pp. 530–535). https://doi.org/http://doi.acm.org/10.1145/378239.379017
  181. Schmitt, S., Lorigo, L., Kreitz, C., & Nogin, A. (2001). JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_34
  182. According, I., Dictionary, O. E., Cd-rom, O. E. D. I. I., & Sos, U. (2000). Handbook of Process Algebra.
  183. Gallian, J. A., & Higgins, A. W. (2000). Helping Students Present Their Research, 289–295.
  184. Riazanov, A., & Voronkov, A. (1999). Vampire. In Automated Deduction — CADE-16: 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings (pp. 292–296). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-48660-7_26
  185. Hurd, J. (1999). Integrating Gandalf and HOL. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_21
  186. Papadimitriou, C. H., & Steiglitz, K. (1998). Combinatorial Optimization: Algorithms and Complexity.
  187. Holt, R. M. (1997). Conceptual Model for Transport Processes in the Culebra Dolomite Member, Rustler Formation Sandia National Laboratories, (August).
  188. Hillenbrand, T., Buch, A., Vogt, R., & Löchner, B. (1997). WALDMEISTER - High-Performance Equational Deduction. Journal of Automated Reasoning, 18(2), 265–270. https://doi.org/10.1023/A:1005872405899
  189. Tammet, T. (1997). Gandalf. Journal of Automated Reasoning, 18(2), 199–204. Retrieved from http://www.scopus.com/inward/record.url?eid=2-s2.0-0031108576&partnerID=tZOtx3y1
  190. Sutcliffe, G. (1996). The Practice of Clausification in Automatic Theorem Proving, (18), 57–68.
  191. Harrison, J. (1996). Proof Style. In E. Giménex & C. Pausin-Mohring (Eds.), Types for Proofs and Programs: International Workshop {TYPES’96} (Vol. 1512, pp. 154–172). Aussois, France: Springer-Verlag.
  192. Tammet, T. (1996). A Resolution Theorem Prover for Intuitionistic Logic (pp. 2–16). Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_65
  193. Yamamoto, M., Nishizaki, S.-ya, Hagiya, M., & Toda, Y. (1995). Formalization of planar graphs. In Higher Order Logic Theorem Proving and Its Applications (pp. 369–384). Berlin, Heidelberg: Springer Berlin Heidelberg. Retrieved from https://goo.gl/FwS1Kv
  194. Zalta, E. N., & Zalta, E. N. (1995). Basic Concepts in Modal Logic. Society, 1–91.
  195. Paulson, L. C. (1994). Isabelle: A Generic Theorem Prover (Vol. 828). Springer Science & Business Media.
  196. van Dalen, D. (1994). Logic and Structure. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-02962-6
  197. Wadler, P. (1993). A taste of linear logic. Lecture Notes in Computer Science, 711(September), 185–210. https://doi.org/10.1007/3-540-57182-5_12
  198. Ingene, C. A., Editorials, G., Editorial, G., Commentaries, G., & Commentary, G. (1993). Manuscript Guidelines, 69(4), 467–468.
  199. Coquand, T. (1992). Pattern matching with dependent types. Informal proceedings of Logical Frameworks. https://doi.org/10.1.1.37.9541
  200. Pitts, A. (1991). Notes on Categorical Logic.
  201. van Benthem, J. (1990). Handbook of Philosophical Logic, Vol. IV: Topics in the Philosophy of Language. Language (Vol. 66, p. 555). https://doi.org/10.2307/414900
  202. Cormen, T., Rivest, R., Leiserson, C., & Stein, C. (1988). Introduction to Algorithms. Molekuliarnaia genetika, mikrobiologiia i virusologiia (pp. 12–16). https://doi.org/10.1163/9789004256064_hao_introduction
  203. Paulson, L. C. (1986). Constructing recursion operators in intuitionistic type theory. Journal of Symbolic Computation, 2(4), 325–355. https://doi.org/10.1016/S0747-7171(86)80002-5
  204. Allen, C., & Moronuki, J. (1984). Haskell programming from principles. Edpacs, 11(7), 15. https://doi.org/10.1080/07366988409450331
  205. Vince, A. (1981). Combinatorial Maps. Journal of Combinatorial Theory, 21, 1–21.
  206. Curry, H. B. (1963). Foundations of mathematical logic. Journal of the Franklin Institute (Vol. 275, p. 438). https://doi.org/10.1016/0016-0032(63)90672-0
  207. Tutte, W. T. (1963). How to Draw a Graph. Proceedings of the London Mathematical Society, s3-13(1), 743–767. https://doi.org/10.1112/plms/s3-13.1.743
  208. Appel, K. I. (1959). Horn Sentences in Identity Theory. The Journal of Symbolic Logic, 24(4), 306–310. Retrieved from http://www.jstor.org/stable/2963901
  209. Church, A. (1940). A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, 5(2), 56–68. https://doi.org/10.2307/2266170
  210. MacLane, S. (1937). A combinatorial condition for planar graphs.
  211. Kuratowski, C. (1930). Sur le probl{è}me des courbes gauches en Topologie. Fundamenta Mathematicae. https://doi.org/10.4064/fm-15-1-271-283
  212. Castillo, C. I. Logica Matematica. 2017.
  213. Book, T. TLDR Pages.
  214. Turaev, V., & Virelizier, A. Monoidal Categories and Topological Field Theory. https://doi.org/10.1007/978-3-319-49834-8
  215. M, N. J. Handbook of writing for the mathematical sciences.pdf.
  216. Lawvere, F. W., & Schanuel, S. H. Conceptual Mathematics: A first introduction to categories.
  217. Harrison, J., Urban, J., & Wiedijk, F. History of Interactive Theorem Proving.
  218. Hales, T. C., Adams, M., Bauer, G., Dang, D. T., Harrison, J., Hoang, T. L., … Zumkeller, R. A formal proof of the Kepler conjecture. ArXiv.
  219. Frumin, D., Geuvers, H., Gondelman, L., & Van Der Weide, N. Finite Sets in Homotopy Type Theory. Retrieved from https://goo.gl/Qm8zp9
  220. Hong, S.-hee, Kaufmann, M., & Kobourov, S. G. Beyond-Planar Graphs : Algorithmics and Combinatorics Edited by, 6(11), 35–62.
  221. De Nivelle, H. Bliksem 1.10 User Manual. Retrieved from https://goo.gl/ZZjaZW
  222. Peter Jan Pahl, R. D. Mathematical Foundations of Computational Engineering: A Handbook. pdf.
  223. Abramsky. Handbook of Logic in Computer Science Mathematical Structures.
  224. Ahrens, B., Capriotti, P., & Spadotti, R. Non-wellfounded trees in Homotopy Type Theory *, (1), 1–12. https://doi.org/10.4230/LIPIcs.TLCA.2015.17