E.W.Ayers

PhD thesis
A Tool for Producing Verified, Explainable Proofs.

Abstract

Mathematicians are reluctant to use interactive theorem provers. In this thesis I argue that this is because proof assistants don't emphasise explanations of proofs; and that in order to produce good explanations, the system must create proofs in a manner that mimics how humans would create proofs. My research goals are to determine what constitutes a human-like proof and to represent human-like reasoning within an interactive theorem prover to create formalised, understandable proofs. Another goal is to produce a framework to visualise the goal states of this system.

To demonstrate this, I present HumanProof: a piece of software built for the Lean 3 theorem prover. It is used for interactively creating proofs that resemble how human mathematicians reason. The system provides a visual, hierarchical representation of the goal and a system for suggesting available inference rules. The system produces output in the form of both natural language and formal proof terms which are checked by Lean's kernel. This is made possible with the use of a structured goal state system which interfaces with Lean's tactic system which is detailed in Chapter 3.

In Chapter 4, I present the subtasks automation planning subsystem, which is used to produce equality proofs in a human-like fashion. The basic strategy of the subtasks system is break a given equality problem in to a hierarchy of tasks and then maintain a stack of these tasks in order to determine the order in which to apply equational rewriting moves. This process produces equality chains for simple problems without having to resort to brute force or specialised procedures such as normalisation. This makes proofs more human-like by breaking the problem into a hierarchical set of tasks in the same way that a human would.

To produce the interface for this software, I also created the ProofWidgets system for Lean 3. This system is detailed in Chapter 5. The ProofWidgets system uses Lean's metaprogramming framework to allow users to write their own interactive, web-based user interfaces to display within the VSCode editor and in an online web-editor. The entire tactic state is available to the rendering engine, and hence expression structure and types of subexpressions can be explored interactively. The ProofWidgets system also allows the user interface to interactively edit the proof document, enabling a truly interactive modality for creating proofs; human-like or not.

In Chapter 6, the system is evaluated by asking real mathematicians about the output of the system, and what it means for a proof to be understandable to them. The user group study asks participants to rank and comment on proofs created by HumanProof alongside natural language and pure Lean proofs. The study finds that participants generally prefer the HumanProof format over the Lean format. The verbal responses collected during the study indicate that providing intuition and signposting are the most important properties of a proof that aid understanding.

Contents

Bibliography

There are 169 bibliography entries.

  • [ABB+16]Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H.; Ulbrich, MattiasDeductive Software Verification - The KeY Book (2016)publisher Springerdoi 10.1007/978-3-319-49812-6isbn 978-3-319-49811-9https://doi.org/10.1007/978-3-319-49812-6
  • [ADL10]Aspinall, David; Denney, Ewen; Lüth, ChristophTactics for hierarchical proof (2010)Mathematics in Computer Sciencevolume 3number 3pages 309--330publisher Springerdoi 10.1007/s11786-010-0025-6https://doi.org/10.1007/s11786-010-0025-6
  • [AGJ19]Ayers, E. W.; Gowers, W. T.; Jamnik, MatejaA human-oriented term rewriting system (2019)KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AIvolume 11793pages 76--86editors Benzmüller, Christoph; Stuckenschmidt, Heinerorganization Springerpublisher Springerdoi 10.1007/978-3-030-30179-8_6https://www.repository.cam.ac.uk/bitstream/handle/1810/298199/main.pdf?sequence=1
  • [AH97]Archer, Myla; Heitmeyer, ConstanceHuman-style theorem proving using PVS (1997)International Conference on Theorem Proving in Higher Order Logicspages 33--48editors Gunter, Elsa L.; Felty, Amy P.organization Springerdoi 10.1007/BFb0028384https://doi.org/10.1007/BFb0028384
  • [AJG21]Ayers, E. W.; Jamnik, Mateja; Gowers, W. T.A graphical user interface framework for formal verification (2021)Interactive Theorem Provingvolume 193pages 4:1--4:16editors Cohen, Liron; Kaliszyk, Cezarypublisher Schloss Dagstuhl - Leibniz-Zentrum für Informatikdoi 10.4230/LIPIcs.ITP.2021.4https://doi.org/10.4230/LIPIcs.ITP.2021.4
  • [ALW07]Aspinall, David; Lüth, Christoph; Winterstein, DanielA framework for interactive proof (2007)Towards Mechanized Mathematical Assistantspages 161--175editors Kauers, Manuel; Kerber, Manfred; Miner, Robert; et al.publisher Springerdoi 10.1007/978-3-540-73086-6_15https://doi.org/10.1007/978-3-540-73086-6_15
  • [AMM18]Adámek, Jiří; Milius, Stefan; Moss, Lawrence SFixed points of functors (2018)Journal of Logical and Algebraic Methods in Programmingvolume 95pages 41--81doi 10.1016/j.jlamp.2017.11.003https://doi.org/10.1016/j.jlamp.2017.11.003
  • [AZHE10]Aigner, Martin; Ziegler, Günter M; Hofmann, Karl H; Erdos, PaulProofs from the Book (2010)publisher Springerisbn 978-3-662-57264-1https://doi.org/10.1007/978-3-662-57265-8
  • [Ano94]AnonymousThe QED manifesto (1994)Automated Deduction--CADEvolume 12pages 238--251http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/wiedijk_2.pdfUnofficially credited as Robert Boyer
  • [Asp00]Aspinall, DavidProof General: A generic tool for proof development (2000)International Conference on Tools and Algorithms for the Construction and Analysis of Systemsvolume 1785pages 38--43editors Graf, Susanne; Schwartzbach, Michael I.organization Springerpublisher Springerdoi 10.1007/3-540-46419-0_3https://link.springer.com/content/pdf/10.1007/3-540-46419-0_3.pdf
  • [BBF+16]Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, AlbertSemi-intelligible Isar proofs from machine-generated proofs (2016)Journal of Automated Reasoningvolume 56number 2pages 155--200publisher Springerdoi 10.1007/s10817-015-9335-3https://doi.org/10.1007/s10817-015-9335-3
  • [BBHI05]Bundy, Alan; Basin, David; Hutter, Dieter; Ireland, AndrewRippling: meta-level guidance for mathematical reasoning (2005)volume 56publisher Cambridge University Pressisbn 978-0-521-83449-0https://books.google.co.uk/books?id=dZzbL-lnjVEC
  • [BCC+13]Bainomugisha, Engineer; Carreton, Andoni Lombide; Cutsem, Tom van; Mostinckx, Stijn; Meuter, Wolfgang deA survey on reactive programming (2013)ACM Computing Surveys (CSUR)volume 45number 4pages 1--34editor Hankin, Chrispublisher ACM New York, NY, USAdoi 10.1145/2501654.2501666https://doi.org/10.1145/2501654.2501666
  • [BCF+97]Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg H.; Sorge, VolkerOmega: Towards a Mathematical Assistant (1997)Automated Deduction - CADE-14volume 1249pages 252--255editor McCune, Williampublisher Springerdoi 10.1007/3-540-63104-6_23https://doi.org/10.1007/3-540-63104-6_23
  • [BCJ+06]Buchberger, Bruno; Crǎciun, Adrian; Jebelean, Tudor; Kovács, Laura; Kutsia, Temur; Nakagawa, Koji; Piroi, Florina; Popov, Nikolaj; Robu, Judit; Rosenkranz, Markus; Windsteiger, WolfgangTheorema: Towards computer-aided mathematical theory exploration (2006)Journal of Applied Logicvolume 4number 4pages 470--504editor Benzmüller, Christophpublisher Elsevierdoi 10.1016/j.jal.2005.10.006https://doi.org/10.1016/j.jal.2005.10.006
  • [BE92]Barwise, Jon; Etchemendy, JohnHyperproof: Logical reasoning with diagrams (1992)Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representationshttps://www.aaai.org/Papers/Symposia/Spring/1992/SS-92-02/SS92-02-016.pdf
  • [BF97]Blum, Avrim L; Furst, Merrick LFast planning through planning graph analysis (1997)Artificial intelligencevolume 90number 1-2pages 281--300editor Bobrow, Daniel G.publisher Elsevierdoi 10.1016/S0004-3702(96)00047-1https://doi.org/10.1016/S0004-3702(96)00047-1
  • [BG01]Bachmair, Leo; Ganzinger, HaraldResolution theorem proving (2001)Handbook of automated reasoningpages 19--99editors Robinson, J. A.; Voronkov, A.publisher Elsevier
  • [BGM+13]Bird, Richard; Gibbons, Jeremy; Mehner, Stefan; Voigtländer, Janis; Schrijvers, TomUnderstanding idiomatic traversals backwards and forwards (2013)Proceedings of the 2013 ACM SIGPLAN symposium on Haskellpages 25--36https://lirias.kuleuven.be/retrieve/237812
  • [BJK+16]Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, WolfgangTheorema 2.0: computer-assisted natural-style mathematics (2016)Journal of Formalized Reasoningvolume 9number 1pages 149--185doi 10.6092/issn.1972-5787/4568https://doi.org/10.6092/issn.1972-5787/4568
  • [BKM95]Boyer, Robert S; Kaufmann, Matt; Moore, J StrotherThe Boyer-Moore theorem prover and its interactive enhancement (1995)Computers & Mathematics with Applicationsvolume 29number 2pages 27--62publisher Elsevier
  • [BM72]Boyer, R. S.; Moore, J. S.The sharing structure in theorem-proving programs (1972)Machine intelligencevolume 7pages 101--116editors Meltzer, B.; Michie, D.publisher Edinburgh University Presshttps://www.cs.utexas.edu/~moore/publications/structure-sharing-mi7.pdf
  • [BM73]Boyer, Robert S.; Moore, J. StrotherProving Theorems about LISP Functions (1973)IJCAIpages 486--493editor Nilsson, Nils J.publisher William Kaufmannhttp://ijcai.org/Proceedings/73/Papers/053.pdf
  • [BM90]Boyer, Robert S; Moore, J StrotherA theorem prover for a computational logic (1990)International Conference on Automated Deductionpages 1--15organization Springerhttps://www.cs.utexas.edu/users/boyer/ftp/cli-reports/054.pdf
  • [BMR+20]Brown, Tom B.; Mann, Benjamin; Ryder, Nick; Subbiah, Melanie; Kaplan, Jared; Dhariwal, Prafulla; Neelakantan, Arvind; Shyam, Pranav; Sastry, Girish; Askell, Amanda; Agarwal, Sandhini; Herbert-Voss, Ariel; Krueger, Gretchen; Henighan, Tom; Child, Rewon; Ramesh, Aditya; Ziegler, Daniel M.; Wu, Jeffrey; Winter, Clemens; Hesse, Christopher; Chen, Mark; Sigler, Eric; Litwin, Mateusz; Gray, Scott; Chess, Benjamin; Clark, Jack; Berner, Christopher; McCandlish, Sam; Radford, Alec; Sutskever, Ilya; Amodei, DarioLanguage Models are Few-Shot Learners (2020)NeurIPSeditors Larochelle, Hugo; Ranzato, Marc'Aurelio; Hadsell, Raia; et al.https://proceedings.neurips.cc/paper/2020/hash/1457c0d6bfcb4967418bfb8ac142f64a-Abstract.html
  • [BN10]Böhme, Sascha; Nipkow, TobiasSledgehammer: judgement day (2010)International Joint Conference on Automated Reasoningpages 107--121editors Giesl, Jürgen; Hähnle, Reinerorganization Springerdoi 10.1007/978-3-642-14203-1_9https://doi.org/10.1007/978-3-642-14203-1_9
  • [BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998)publisher Cambridge University Pressisbn 978-0-521-45520-6
  • [BSV+93]Bundy, Alan; Stevens, Andrew; Van Harmelen, Frank; Ireland, Andrew; Smaill, AlanRippling: A heuristic for guiding inductive proofs (1993)Artificial Intelligencevolume 62number 2pages 185--253publisher Elsevierdoi 10.1016/0004-3702(93)90079-Qhttps://doi.org/10.1016/0004-3702(93)90079-Q
  • [BT98]Bertot, Yves; Théry, LaurentA generic approach to building user interfaces for theorem provers (1998)Journal of Symbolic Computationvolume 25number 2pages 161--194publisher Elsevierdoi 10.1006/jsco.1997.0171https://doi.org/10.1006/jsco.1997.0171
  • [Bau20]Bauer, AndrejWhat makes dependent type theory more suitable than set theory for proof assistants? (2020)https://mathoverflow.net/q/376973MathOverflow answer
  • [Bil05]Bille, PhilipA survey on tree edit distance and related problems (2005)Theoretical computer sciencevolume 337number 1-3pages 217--239publisher Elsevierdoi 10.1016/j.tcs.2004.12.030https://doi.org/10.1016/j.tcs.2004.12.030
  • [Ble81]Bledsoe, Woodrow WNon-resolution theorem proving (1981)Readings in Artificial Intelligencepages 91--108editor Meltzer, Bernardpublisher Elsevierdoi 10.1016/0004-3702(77)90012-1https://doi.org/10.1016/0004-3702(77)90012-1
  • [Bre16]Breitner, JoachimVisual theorem proving with the Incredible Proof Machine (2016)International Conference on Interactive Theorem Provingpages 123--139editors Blanchette, Jasmin Christian; Merz, Stephanpublisher Springerdoi 10.1007/978-3-319-43144-4_8https://www.info.uni-karlsruhe.de/uploads/publikationen/breitner16incredible.pdf
  • [Bun02]Bundy, AlanA critique of proof planning (2002)Computational Logic: Logic Programming and Beyondpages 160--177editors Kakas, Antonis C.; Sadri, Faribapublisher Springerdoi 10.1007/3-540-45632-5_7https://doi.org/10.1007/3-540-45632-5_7
  • [Bun11]Bundy, AlanAutomated theorem provers: a practical tool for the working mathematician? (2011)Annals of Mathematics and Artificial Intelligencevolume 61number 1pages 3--14doi 10.1007/s10472-011-9248-8https://doi.org/10.1007/s10472-011-9248-8
  • [Bun88]Bundy, AlanThe use of explicit plans to guide inductive proofs (1988)International conference on automated deductionvolume 310pages 111--120editors Lusk, Ewing L.; Overbeek, Ross A.organization Springerpublisher Springerdoi 10.1007/BFb0012826https://doi.org/10.1007/BFb0012826
  • [Bun98]Bundy, AlanProof Planning (1998)publisher University of Edinburgh, Department of Artificial Intelligencehttps://books.google.co.uk/books?id=h7hrHAAACAAJ
  • [CC13]Czaplicki, Evan; Chong, StephenAsynchronous functional reactive programming for GUIs (2013)ACM SIGPLAN Conference on Programming Language Design and Implementationpages 411--422editors Boehm, Hans-Juergen; Flanagan, Cormacpublisher ACMdoi 10.1145/2491956.2462161https://doi.org/10.1145/2491956.2462161
  • [CFK+09]Cramer, Marcos; Fisseni, Bernhard; Koepke, Peter; Kühlwein, Daniel; Schröder, Bernhard; Veldman, JipThe Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts (2009)Controlled Natural Language, Workshop on Controlled Natural Languagevolume 5972pages 170--186editor Fuchs, Norbert E.publisher Springerdoi 10.1007/978-3-642-14418-9_11https://doi.org/10.1007/978-3-642-14418-9_11
  • [CH88]Coquand, Thierry; Huet, Gérard P.The Calculus of Constructions (1988)Information and Computationvolume 76number 2/3pages 95--120publisher Elsevierdoi 10.1016/0890-5401(88)90005-3https://doi.org/10.1016/0890-5401(88)90005-3
  • [CL18]Choi, Dongkyu; Langley, PatEvolution of the ICARUS cognitive architecture (2018)Cognitive Systems Researchvolume 48pages 25--38publisher Elsevierdoi 10.1016/j.cogsys.2017.05.005https://doi.org/10.1016/j.cogsys.2017.05.005
  • [CMM+17]Corneli, Joseph; Martin, Ursula; Murray-Rust, Dave; Pease, Alison; Puzio, Raymond; Rino Nesin, GabrielaModelling the way mathematics is actually done (2017)Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Designpages 10--19editors Sperber, Michael; Bresson, Jeanorganization ACMpublisher ACMdoi 10.1145/3122938.3122942https://doi.org/10.1145/3122938.3122942
  • [Car19]Carneiro, MarioLean's Type Theory (2019)https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf
  • [Chu18]Chua, DexterCambridge Notes (2018)https://dec41.user.srcf.net/notesGitHub: https://github.com/dalcde/cam-notes
  • [Com20]The Mathlib CommunityThe Lean Mathematical Library (2020)Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofspages 367–381publisher Association for Computing Machinerydoi 10.1145/3372885.3373824isbn 9781450370974https://doi.org/10.1145/3372885.3373824
  • [Coq]The Coq Development TeamThe Coq Reference Manual (2021)https://coq.inria.fr/distrib/current/refman/#
  • [DH93]Dalianis, Hercules; Hovy, EduardAggregation in natural language generation (1993)European Workshop on Trends in Natural Language Generationvolume 1036pages 88--105editors Adorni, Giovanni; Zock, Michaelorganization Springerpublisher Springerdoi 10.1007/3-540-60800-1_25https://doi.org/10.1007/3-540-60800-1_25
  • [DJP06]Dennis, Louise A; Jamnik, Mateja; Pollet, MartinOn the Comparison of Proof Planning Systems: lambdaCLAM, Ωmega and IsaPlanner (2006)Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoningvolume 151number 1pages 93--110editors Carette, Jacques; Farmer, William M.publisher Elsevierdoi 10.1016/j.entcs.2005.11.025https://www.cl.cam.ac.uk/~mj201/publications/comp_pp_final.pdf
  • [DKL20]De Lon, Adrian; Koepke, Peter; Lorenzen, AntonInterpreting Mathematical Texts in Naproche-SAD (2020)Intelligent Computer Mathematicspages 284--289editors Benzmüller, Christoph; Miller, Brucepublisher Springer International Publishingdoi 10.1007/978-3-030-53518-6_19isbn 978-3-030-53518-6https://doi.org/10.1007/978-3-030-53518-6_19
  • [Dav09]Davis, Jared CurranA self-verifying theorem prover (2009)https://search.proquest.com/openview/96fda9a67e5fa11fb241ebf4984c7368/1?pq-origsite=gscholar&cbl=18750
  • [DeB80]De Bruijn, Nicolaas GovertA survey of the project AUTOMATH (1980)To H.B.Curry: Essays on Combinatory Logic,Lambda Calculus and Formalismpages 579-606editors Hindley, J.R.; Seldin, J.P.publisher Academic Presshttps://research.tue.nl/files/2092478/597605.pdf
  • [Dow01]Dowek, GilesHigher-order unification and matching (2001)Handbook of automated reasoningvolume 2pages 1009--1063editors Robinson, Alan; Voronkov, Andreipublisher Elsevier
  • [EH97]Elliott, Conal; Hudak, PaulFunctional reactive animation (1997)Proceedings of the second ACM SIGPLAN international conference on Functional programmingpages 263--273editors Peyton Jones, Simon L.; Tofte, Mads; Berman, A. Michaeldoi 10.1145/258948.258973https://doi.org/10.1145/258948.258973
  • [EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; Avigad, Jeremy; de Moura, LeonardoA metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languagesvolume 1number ICFPpages 1--29editor Wadler, Philippublisher ACM New York, NY, USAdoi 10.1145/3110278https://doi.org/10.1145/3110278
  • [Edg07]Edgar, GeraldMeasure, topology, and fractal geometry (2007)publisher Springer
  • [Ell01]Elliott, ConalFunctional Image Synthesis (2001)Proceedings of Bridgeshttp://conal.net/papers/bridges2001/
  • [FGM+07]Foster, J Nathan; Greenwald, Michael B; Moore, Jonathan T; Pierce, Benjamin C; Schmitt, AlanCombinators for bidirectional tree transformations: A linguistic approach to the view-update problem (2007)ACM Transactions on Programming Languages and Systems (TOPLAS)volume 29number 3pages 17--espublisher ACM New York, NY, USAhttps://hal.inria.fr/inria-00484971/file/lenses-toplas-final.pdf
  • [FM87]Felty, Amy; Miller, DaleProof explanation and revision (1987)number MS-CIS-88-17institution University of Pennsylvaniahttps://repository.upenn.edu/cgi/viewcontent.cgi?article=1660&context=cis_reports
  • [Fle19]Flet-Berliac, YannisThe Promise of Hierarchical Reinforcement Learning (2019)The Gradienthttps://thegradient.pub/the-promise-of-hierarchical-reinforcement-learning
  • [GAA+13]Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Biha, Sidi Ould; othersA machine-checked proof of the odd order theorem (2013)International Conference on Interactive Theorem Provingpages 163--179organization Springerhttps://hal.inria.fr/docs/00/81/66/99/PDF/main.pdf
  • [GFA09]Grossman, Tovi; Fitzmaurice, George W.; Attar, RamtinA survey of software learnability: metrics, methodologies and guidelines (2009)Proceedings of the 27th International Conference on Human Factors in Computing Systemspages 649--658editors Olsen, Dan R. Jr.; Arthur, Richard B.; Hinckley, Ken; et al.publisher ACMdoi 10.1145/1518701.1518803https://doi.org/10.1145/1518701.1518803
  • [GG17]Ganesalingam, Mohan; Gowers, W. T.A fully automatic theorem prover with human-style output (2017)Journal of Automated Reasoningvolume 58number 2pages 253--291doi 10.1007/s10817-016-9377-1https://doi.org/10.1007/s10817-016-9377-1
  • [GK18]Gatt, Albert; Krahmer, EmielSurvey of the state of the art in natural language generation: Core tasks, applications and evaluation (2018)Journal of Artificial Intelligence Researchvolume 61pages 65--170doi 10.1613/jair.5477https://doi.org/10.1613/jair.5477
  • [GKN15]Grabowski, Adam; Korniłowicz, Artur; Naumowicz, AdamFour decades of Mizar (2015)Journal of Automated Reasoningvolume 55number 3pages 191--198editors Trybulec, Andrzej; Trybulec Kuperberg, Krystynapublisher Springerdoi 10.1007/s10817-015-9345-1https://doi.org/10.1007/s10817-015-9345-1
  • [GM05]Grégoire, Benjamin; Mahboubi, AssiaProving equalities in a commutative ring done right in Coq (2005)International Conference on Theorem Proving in Higher Order Logicsvolume 3603pages 98--113editors Hurd, Joe; Melham, Thomas F.organization Springerdoi 10.1007/11541868_7http://cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf
  • [GPJ17]Gallego Arias, Emilio Jesús; Pin, Benoît; Jouvelot, PierrejsCoq: Towards Hybrid Theorem Proving Interfaces (2017)Proceedings of the 12th Workshop on User Interfaces for Theorem Proversvolume 239pages 15-27editors Autexier, Serge; Quaresma, Pedropublisher Open Publishing Associationdoi 10.4204/EPTCS.239.2https://arxiv.org/pdf/1701.07125
  • [Gal16]Gallego Arias, Emilio JesúsSerAPI: Machine-Friendly, Data-Centric Serialization for Coq (2016)institution MINES ParisTechhttps://hal-mines-paristech.archives-ouvertes.fr/hal-01384408/file/serapi.pdf
  • [Gan10]Ganesalingam, MohanThe language of mathematics (2010)publisher Springerdoi 10.1007/978-3-642-37012-0isbn 978-3-642-37011-3http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.211.9027&rep=rep1&type=pdf
  • [Gon08]Gonthier, GeorgesFormal proof--the four-color theorem (2008)Notices of the AMSvolume 55number 11pages 1382--1393editor Magid, Andy
  • [Gor00]Gordon, MikeFrom LCF to HOL: a short history (2000)Proof, language, and interactionpages 169--186editors Plotkin, Gordon D.; Stirling, Colin; Tofte, Madsdoi 10.1.1.132.8662isbn 9780262161886http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.132.8662&rep=rep1&type=pdf
  • [Gow10]Gowers, W. T.Rough structure and classification (2010)Visions in Mathematicspages 79--117publisher Springerhttps://www.dpmms.cam.ac.uk/~wtg10/gafavisions.ps
  • [Gre19]Grebing, Sarah CaeciliaUser Interaction in Deductive Interactive Program Verification (2019)https://d-nb.info/1198309989/34
  • [Gri75]Grice, Herbert PLogic and conversation (1975)Speech actspages 41--58publisher Brillhttp://rrt2.neostrada.pl/mioduszewska/course_265_reading%201b.pdf
  • [HAB+17]Hales, Thomas C; Adams, Mark; Bauer, Gertrud; Dang, Dat Tat; Harrison, John; Hoang, Truong Le; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Thang Tat; Nguyen, Truong Quang; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason M.; Solovyev, Alexey; Ta, An Hoai Thi; Tran, Trung Nam; Trieu, Diep Thi; Urban, Josef; Vu, Ky Khac; Zumkeller, RolandA formal proof of the Kepler conjecture (2017)Forum of Mathematics, Pivolume 5organization Cambridge University Pressdoi doi:10.1017/fmp.2017.1https://doi.org/doi:10.1017/fmp.2017.1
  • [HBC99]Holland-Minkley, Amanda M; Barzilay, Regina; Constable, Robert LVerbalization of High-Level Formal Proofs. (1999)AAAI/IAAIpages 277--284editors Hendler, Jim; Subramanian, Devikapublisher AAAI Press / The MIT Presshttp://www.aaai.org/Library/AAAI/1999/aaai99-041.php
  • [HF97]Huang, Xiaorong; Fiedler, ArminProof Verbalization as an Application of NLG (1997)International Joint Conference on Artificial Intelligencepages 965--972http://ijcai.org/Proceedings/97-2/Papers/025.pdf
  • [HHPW96]Hall, Cordelia V; Hammond, Kevin; Peyton Jones, Simon L; Wadler, Philip LType classes in Haskell (1996)ACM Transactions on Programming Languages and Systems (TOPLAS)volume 18number 2pages 109--138publisher ACM New York, NY, USAdoi 10.1145/227699.227700https://doi.org/10.1145/227699.227700
  • [HRW+21]Han, Jesse Michael; Rute, Jason; Wu, Yuhuai; Ayers, Edward W; Polu, StanislasProof Artifact Co-training for Theorem Proving with Language Models (2021)arXiv preprint arXiv:2102.06203https://arxiv.org/pdf/2102.06203
  • [Hal05]Hales, Thomas CA proof of the Kepler conjecture (2005)Annals of mathematicspages 1065--1185publisher Mathematics Department, Princeton Universityhttp://annals.math.princeton.edu/wp-content/uploads/annals-v162-n3-p01.pdf
  • [Hal07]Hales, Thomas CThe Jordan curve theorem, formally and informally (2007)The American Mathematical Monthlyvolume 114number 10pages 882--894publisher Taylor & Francishttps://www.maths.ed.ac.uk/~v1ranick/papers/hales3.pdf
  • [Har09]Harrison, JohnHOL Light: An Overview. (2009)TPHOLsvolume 5674pages 60--66editors Berghofer, Stefan; Nipkow, Tobias; Urban, Christian; et al.organization Springerdoi 10.1007/978-3-642-03359-9_4https://doi.org/10.1007/978-3-642-03359-9_4
  • [Hue97]Huet, GérardFunctional Pearl: The Zipper (1997)Journal of functional programmingvolume 7number 5pages 549--554publisher Cambridge University Presshttp://www.st.cs.uni-sb.de/edu/seminare/2005/advanced-fp/docs/huet-zipper.pdf
  • [Hur95]Hurkens, Antonius J. C.A simplification of Girard's paradox (1995)International Conference on Typed Lambda Calculi and Applicationspages 266--278editors Dezani-Ciancaglini, Mariangiola; Plotkin, Gordon D.organization Springerdoi 10.1007/BFb0014058https://doi.org/10.1007/BFb0014058
  • [IA12]Inglis, Matthew; Alcock, LaraExpert and novice approaches to reading mathematical proofs (2012)Journal for Research in Mathematics Educationvolume 43number 4pages 358--390publisher National Council of Teachers of Mathematicshttps://pdfs.semanticscholar.org/494e/7981ee892d500139708e53901d6260bd83b1.pdf
  • [IJR99]Ireland, Andrew; Jackson, Michael; Reid, GordonInteractive proof critics (1999)Formal Aspects of Computingvolume 11number 3pages 302--325publisher Springerdoi 10.1007/s001650050052https://doi.org/10.1007/s001650050052
  • [Ire92]Ireland, AndrewThe use of planning critics in mechanizing inductive proofs (1992)International Conference on Logic for Programming Artificial Intelligence and Reasoningpages 178--189editor Voronkov, Andreiorganization Springerdoi 10.1007/BFb0013060http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.40.3546&rep=rep1&type=pdf
  • [JR12]Jaskelioff, Mauro; Rypacek, OndrejAn Investigation of the Laws of Traversals (2012)Proceedings Fourth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2012, Tallinn, Estoniavolume 76pages 40--49editors Chapman, James; Levy, Paul Blaindoi 10.4204/EPTCS.76.5https://doi.org/10.4204/EPTCS.76.5
  • [Jam01]Jamnik, MatejaMathematical Reasoning with Diagrams: From Intuition to Automation (2001)publisher CSLI Pressisbn 9781575863238
  • [KB70]Knuth, Donald E; Bendix, Peter BSimple word problems in universal algebras (1970)Computational Problems in Abstract Algebrapages 263-297editor Leech, Johnpublisher Pergamondoi https://doi.org/10.1016/B978-0-08-012975-4.50028-Xisbn 978-0-08-012975-4https://www.cs.tufts.edu/~nr/cs257/archive/don-knuth/knuth-bendix.pdf
  • [KEH+09]Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, SimonseL4: Formal verification of an OS kernel (2009)Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principlespages 207--220editors Matthews, Jeanna Neefe; Anderson, Thomas E.organization ACMdoi 10.1145/1629575.1629596https://doi.org/10.1145/1629575.1629596
  • [KKY95]Kambhampati, Subbarao; Knoblock, Craig A; Yang, QiangPlanning as refinement search: A unified framework for evaluating design tradeoffs in partial-order planning (1995)Artificial Intelligencevolume 76number 1pages 167--238doi 10.1016/0004-3702(94)00076-Dhttps://doi.org/10.1016/0004-3702(94)00076-D
  • [KMM13]Kaufmann, Matt; Manolios, Panagiotis; Moore, J StrotherComputer-aided reasoning: ACL2 case studies (2013)volume 4publisher Springer
  • [KSFS05]Kiselyov, Oleg; Shan, Chung-chieh; Friedman, Daniel P; Sabry, AmrBacktracking, interleaving, and terminating monad transformers: (functional pearl) (2005)ACM SIGPLAN Noticesvolume 40number 9pages 192--203editors Danvy, Olivier; Pierce, Benjamin C.publisher ACM New York, NY, USAdoi 10.1145/1086365.1086390https://doi.org/10.1145/1086365.1086390
  • [Knu86]Knuth, Donald E.The TeXbook (1986)publisher Addison-Wesleyisbn 0-201-13447-0
  • [Kuh14]Kuhn, TobiasA survey and classification of controlled natural languages (2014)Computational linguisticsvolume 40number 1pages 121--170publisher MIT Pressdoi 10.1162/COLI_a_00168https://doi.org/10.1162/COLI_a_00168
  • [LC20]Lample, Guillaume; Charton, FrançoisDeep Learning For Symbolic Mathematics (2020)ICLRpublisher OpenReview.nethttps://openreview.net/forum?id=S1eZYeHFDS
  • [LCT08]Langley, Pat; Choi, Dongkyu; Trivedi, NishantIcarus user’s manual (2008)institution Institute for the Study of Learning and Expertisehttp://www.isle.org/~langley/papers/manual.pdf
  • [LD97]Lowe, Helen; Duncan, DavidXBarnacle: Making Theorem Provers More Accessible (1997)14th International Conference on Automated Deductionvolume 1249pages 404--407editor McCune, Williampublisher Springerdoi 10.1007/3-540-63104-6_39https://doi.org/10.1007/3-540-63104-6_39
  • [LP03]Lämmel, Ralf; Peyton Jones, SimonScrap Your Boilerplate (2003)Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedingsvolume 2895pages 357editor Ohori, Atsushipublisher Springerdoi 10.1007/978-3-540-40018-9_23https://doi.org/10.1007/978-3-540-40018-9_23
  • [LR13]Lüth, Christoph; Ring, MartinA web interface for Isabelle: The next generation (2013)International Conference on Intelligent Computer Mathematicspages 326--329organization Springerhttp://www.informatik.uni-bremen.de/~clueth/papers/cicm2013.pdf
  • [LYWP21]Li, Wenda; Yu, Lei; Wu, Yuhuai; Paulson, Lawrence C.IsarStep: a Benchmark for High-level Mathematical Reasoning (2021)International Conference on Learning Representationshttps://openreview.net/forum?id=Pzj6fzU6wkj
  • [Lew17]Lewis, Robert Y.An Extensible Ad Hoc Interface between Lean and Mathematica (2017)Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017volume 262pages 23--37editors Dubois, Catherine; Paleo, Bruno Woltzenlogeldoi 10.4204/EPTCS.262.4https://doi.org/10.4204/EPTCS.262.4
  • [Low97]Lowe, HelenEvaluation of a Semi-Automated Theorem Prover (Part I) (1997)https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.48.2318&rep=rep1&type=pdf
  • [MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; Roux, CodyElaboration in Dependent Type Theory (2015)CoRRvolume abs/1505.04324http://arxiv.org/abs/1505.04324
  • [MB08]de Moura, Leonardo; Bjørner, NikolajZ3: An efficient SMT solver (2008)International conference on Tools and Algorithms for the Construction and Analysis of Systemspages 337--340editors Ramakrishnan, C. R.; Rehof, Jakoborganization Springerdoi 10.1007/978-3-540-78800-3_24https://doi.org/10.1007/978-3-540-78800-3_24
  • [MH93]Monk, Andrew; Haber, JeanneImproving your human-computer interface: a practical technique (1993)publisher Prentice Hallisbn 9780130100344https://books.google.co.uk/books?id=JN9QAAAAMAAJ
  • [MKA+15]de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; Van Doorn, Floris; von Raumer, JakobThe Lean theorem prover (system description) (2015)International Conference on Automated Deductionvolume 9195pages 378--388editors Felty, Amy P.; Middeldorp, Aartorganization Springerdoi 10.1007/978-3-319-21401-6_26https://kilthub.cmu.edu/articles/The_Lean_Theorem_Prover_system_description_/6492815/files/11937416.pdf
  • [MP08]McBride, Conor; Paterson, RossApplicative programming with effects (2008)J. Funct. Program.volume 18number 1pages 1--13doi 10.1017/S0956796807006326https://personal.cis.strath.ac.uk/conor.mcbride/IdiomLite.pdf
  • [MS99]Melis, Erica; Siekmann, JörgKnowledge-based proof planning (1999)Artificial Intelligencevolume 115number 1pages 65--105editor Bobrow, Daniel G.publisher Elsevierdoi 10.1016/S0004-3702(99)00076-4https://doi.org/10.1016/S0004-3702(99)00076-4
  • [MUP79]de Millo, Richard A; Upton, Richard J; Perlis, Alan JSocial processes and proofs of theorems and programs (1979)Communications of the ACMvolume 22number 5pages 271--280doi 10.1145/359104.359106https://doi.org/10.1145/359104.359106
  • [Mar84]Martin-Löf, PerIntuitionistic type theory (1984)volume 1publisher Bibliopolisisbn 978-88-7088-228-5http://people.csail.mit.edu/jgross/personal-website/papers/academic-papers-local/Martin-Lof80.pdf
  • [McB00]McBride, ConorDependently typed functional programs and their proofs (2000)http://hdl.handle.net/1842/374
  • [McC60]McCarthy, JohnRecursive functions of symbolic expressions and their computation by machine, Part I (1960)Communications of the ACMvolume 3number 4pages 184--195publisher ACM New York, NY, USAdoi 10.1145/367177.367199https://doi.org/10.1145/367177.367199
  • [Mic78]Michener, Edwina RisslandUnderstanding understanding mathematics (1978)Cognitive sciencevolume 2number 4pages 361--383publisher Wiley Online Librarydoi https://doi.org/10.1207/s15516709cog0204_3https://onlinelibrary.wiley.com/doi/pdf/10.1207/s15516709cog0204_3
  • [Mil72]Milner, RobinLogic for computable functions description of a machine implementation (1972)institution Stanford Universityhttps://apps.dtic.mil/dtic/tr/fulltext/u2/785072.pdf
  • [Nev74]Nevins, Arthur JA human oriented logic for automatic theorem-proving (1974)Journal of the ACMvolume 21number 4pages 606--621publisher ACM New York, NY, USAdoi 10.1145/321850.321858https://doi.org/10.1145/321850.321858
  • [Nor08]Norell, UlfDependently typed programming in Agda (2008)International school on advanced functional programmingvolume 5832pages 230--266editors Koopman, Pieter W. M.; Plasmeijer, Rinus; Swierstra, S. Doaitseorganization Springerdoi 10.1007/978-3-642-04652-0_5https://doi.org/10.1007/978-3-642-04652-0_5
  • [PLB+17]Pease, Alison; Lawrence, John; Budzynska, Katarzyna; Corneli, Joseph; Reed, ChrisLakatos-style collaborative mathematics through dialectical, structured and abstract argumentation (2017)Artificial Intelligencevolume 246pages 181--219publisher Elsevierdoi 10.1016/j.artint.2017.02.006https://www.sciencedirect.com/science/article/pii/S0004370217300267
  • [PP89]Pfenning, Frank; Paulin-Mohring, ChristineInductively defined types in the Calculus of Constructions (1989)International Conference on Mathematical Foundations of Programming Semanticspages 209--228organization Springerhttps://kilthub.cmu.edu/ndownloader/files/12096983
  • [Pas07]Paskevich, AndreiThe syntax and semantics of the ForTheL language (2007)http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.211.8865&rep=rep1&type=pdfEnglish translation of a portion of Paskevich's PhD thesis
  • [Pau89]Paulson, Lawrence CThe foundation of a generic theorem prover (1989)Journal of Automated Reasoningvolume 5number 3pages 363--397doi 10.1007/BF00248324https://doi.org/10.1007/BF00248324
  • [Pau98]Paulson, Lawrence CThe inductive approach to verifying cryptographic protocols (1998)Journal of Computer Securityvolume 6number 1-2pages 85--128http://content.iospress.com/articles/journal-of-computer-security/jcs102
  • [Pau99]Paulson, Lawrence CA generic tableau prover and its integration with Isabelle (1999)Journal of Universal Computer Sciencevolume 5number 3pages 73--87doi 10.3217/jucs-005-03-0073https://doi.org/10.3217/jucs-005-03-0073
  • [Pit20]Pit-Claudel, ClémentUntangling mechanized proofs (2020)SLE 2020: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineeringpages 155--174doi 10.1145/3426425.3426940https://doi.org/10.1145/3426425.3426940
  • [Poi14]Poincaré, HenriScience and method (1914)translator Halsted, George Brucepublisher Amazon (out of copyright)isbn 978-1534945906https://archive.org/details/sciencemethod00poinuoftThe version at URL is translated by Francis Maitland
  • [Pro13]The Univalent Foundations ProgramHomotopy Type Theory: Univalent Foundations of Mathematics (2013)publisher Institute for Advanced Studyhttps://homotopytypetheory.org/book/
  • [Pól62]Pólya, GeorgeMathematical Discovery (1962)publisher John Wiley & Sonshttps://archive.org/details/GeorgePolyaMathematicalDiscovery
  • [RD00]Reiter, Ehud; Dale, RobertBuilding natural language generation systems (2000)publisher Cambridge University Presshttps://dl.acm.org/doi/book/10.5555/331955
  • [RN10]Russell, Stuart J.; Norvig, PeterArtificial Intelligence - A Modern Approach (2010)publisher Pearson Educationisbn 978-0-13-207148-2http://aima.cs.berkeley.edu/
  • [RSS+20]Raggi, Daniel; Stapleton, Gem; Stockdill, Aaron; Jamnik, Mateja; Garcia, Grecia Garcia; Cheng, Peter C.-H.How to (Re)represent it? (2020)32nd IEEE International Conference on Tools with Artificial Intelligencepages 1224--1232publisher IEEEdoi 10.1109/ICTAI50040.2020.00185https://doi.org/10.1109/ICTAI50040.2020.00185
  • [RV02]Riazanov, Alexandre; Voronkov, AndreiThe design and implementation of VAMPIRE (2002)AI communicationsvolume 15number 2-3pages 91--110http://content.iospress.com/articles/ai-communications/aic259
  • [Ran94]Ranta, AarneSyntactic categories in the language of mathematics (1994)International Workshop on Types for Proofs and Programspages 162--182editors Dybjer, Peter; Nordström, Bengt; Smith, Jan M.organization Springerdoi 10.1007/3-540-60579-7_9https://doi.org/10.1007/3-540-60579-7_9
  • [Ran95]Ranta, AarneContext-relative syntactic categories and the formalization of mathematical text (1995)International Workshop on Types for Proofs and Programspages 231--248editors Berardi, Stefano; Coppo, Marioorganization Springerdoi 10.1007/3-540-61780-9_73http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.8663&rep=rep1&type=pdf
  • [Ros53]Rosser, J. BarkleyLogic for Mathematicians (1953)publisher McGraw-Hillisbn 978-0-486-46898-3
  • [SB01]Snyder, Wayne; Baader, FranzUnification theory (2001)Handbook of automated reasoningvolume 1pages 447--533editors Robinson, Alan; Voronkov, Andreipublisher Elsevier
  • [SB18a]Steen, Alexander; Benzmüller, ChristophThe higher-order prover Leo-III (2018)International Joint Conference on Automated Reasoningvolume 10900pages 108--116editors Galmiche, Didier; Schulz, Stephan; Sebastiani, Robertopublisher Springerdoi 10.1007/978-3-319-94205-6_8https://doi.org/10.1007/978-3-319-94205-6_8
  • [SB18b]Sutton, Richard S; Barto, Andrew GReinforcement learning: An introduction (2018)publisher MIT presshttp://incompleteideas.net/book/the-book-2nd.html
  • [SBRT18]Stathopoulos, Yiannos; Baker, Simon; Rei, Marek; Teufel, SimoneVariable Typing: Assigning Meaning to Variables in Mathematical Text (2018)NAACL-HLT 2018pages 303--312editors Walker, Marilyn A.; Ji, Heng; Stent, Amandapublisher Association for Computational Linguisticsdoi 10.18653/v1/n18-1028https://doi.org/10.18653/v1/n18-1028
  • [SCO95]Stenning, Keith; Cox, Richard; Oberlander, JonContrasting the cognitive effects of graphical and sentential logic teaching: reasoning, representation and individual differences (1995)Language and Cognitive Processesvolume 10number 3-4pages 333--354publisher Taylor & Francishttp://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.49.3906&rep=rep1&type=pdf
  • [SCV19]Schulz, Stephan; Cruanes, Simon; Vukmirović, PetarFaster, Higher, Stronger: E 2.3 (2019)Proc. of the 27th CADE, Natal, Brasilnumber 11716pages 495--507editor Fontaine, Pascalpublisher Springerhttp://wwwlehre.dhbw-stuttgart.de/~sschulz/bibliography.html#SCV:CADE-2019
  • [SH17]Sterling, Jonathan; Harper, RobertAlgebraic Foundations of Proof Refinement (2017)CoRRvolume abs/1703.05215http://arxiv.org/abs/1703.05215
  • [SHB+99]Siekmann, Jörg; Hess, Stephan; Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fiedler, Armin; Horacek, Helmut; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Pollet, Martin; Sorge, VolkerLOUI: Lovely OMEGA user interface (1999)Formal Aspects of Computingvolume 11number 3pages 326--342editor Woodcock, Jamespublisher Springerdoi 10.1007/s001650050053https://doi.org/10.1007/s001650050053
  • [SORS01]Shankar, Natarajan; Owre, Sam; Rushby, John M; Stringer-Calvert, Dave WJPVS prover guide (2001)Computer Science Laboratory, SRI International, Menlo Park, CAhttps://pvs.csl.sri.com/doc/pvs-prover-guide.pdf
  • [SP82]Smyth, Michael B; Plotkin, Gordon DThe category-theoretic solution of recursive domain equations (1982)SIAM Journal on Computingvolume 11number 4pages 761--783publisher SIAMhttp://wrap.warwick.ac.uk/46312/1/WRAP_Smyth_cs-rr-014.pdf
  • [SRV01]Sekar, R; Ramakrishnan, I.V.; Voronkov, AndreiTerm Indexing (2001)Handbook of automated reasoningvolume 2pages 1855--1900editors Robinson, Alan; Voronkov, Andreipublisher Elsevier
  • [ST16]Stathopoulos, Yiannos A; Teufel, SimoneMathematical information retrieval based on type embeddings and query expansion (2016)COLING 2016pages 2344--2355editors Calzolari, Nicoletta; Matsumoto, Yuji; Prasad, Rashmipublisher ACLhttps://www.aclweb.org/anthology/C16-1221/
  • [Sac74]Sacerdoti, Earl DPlanning in a hierarchy of abstraction spaces (1974)Artificial intelligencevolume 5number 2pages 115--135publisher Elsevierdoi 10.1016/0004-3702(74)90026-5https://doi.org/10.1016/0004-3702(74)90026-5
  • [Sch12]Schreier, MargritQualitative content analysis in practice (2012)publisher SAGE Publicationsisbn 9781849205931https://uk.sagepub.com/en-gb/eur/qualitative-content-analysis-in-practice/book234633
  • [Sie90]Sierpinska, AnnaSome remarks on understanding in mathematics (1990)For the learning of mathematicsvolume 10number 3pages 24--41publisher FLM Publishing Associationhttps://www.flm-journal.org/Articles/43489F40454C8B2E06F334CC13CCA8.pdf
  • [Sie94]Sierpinska, AnnaUnderstanding in mathematics (1994)volume 2publisher Psychology Pressisbn 9780750705684
  • [Spi11]Spiwack, ArnaudVerified computing in homological algebra, a journey exploring the power and limits of dependent type theory (2011)https://pastel.archives-ouvertes.fr/pastel-00605836/document
  • [Spi87]Spinoza, BenedictThe chief works of Benedict de Spinoza (1887)translator Elwes, R.H.M.publisher Chiswick Presshttps://books.google.co.uk/books?id=tnl09KVEd2UC&ots=WiBRHdjSjY&dq=the%20philosophy%20of%20benedict%20spinoza&lr&pg=PA3#v=onepage&q&f=false
  • [Ste17]Steele Jr., Guy L.It's Time for a New Old Language (2017)http://2017.clojure-conj.org/guy-steele/Invited talk at Clojure/Conj 2017. Slides: http://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf
  • [Tat77]Tate, AustinGenerating project networks (1977)Proceedings of the 5th International Joint Conference on Artificial Intelligence.pages 888--893editor Reddy, Rajorganization Morgan Kaufmann Publishers Inc.doi 10.5555/1622943.1623021https://dl.acm.org/doi/abs/10.5555/1622943.1623021
  • [Tho92]Thomassen, CarstenThe Jordan-Schönflies theorem and the classification of surfaces (1992)The American Mathematical Monthlyvolume 99number 2pages 116--130publisher Taylor & Francishttps://www.jstor.org/stable/2324180
  • [UM20]Ullrich, Sebastian; de Moura, LeonardoBeyond Notations: Hygienic Macro Expansion for Theorem Proving Languages (2020)Automated Reasoningpages 167--182editors Peltier, Nicolas; Sofronie-Stokkermans, Vioricapublisher Springer International Publishingdoi 10.1007/978-3-030-51054-1_10https://doi.org/10.1007/978-3-030-51054-1_10
  • [VKB18]Vicary, Jamie; Kissinger, Aleks; Bar, KrzysztofGlobular: an online proof assistant for higher-dimensional rewriting (2018)Logical Methods in Computer Sciencevolume 14publisher Episciences.orghttps://core.ac.uk/download/pdf/79162392.pdfproject website: http://ncatlab.org/nlab/show/Globular
  • [VLP07]Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, AndreiSystem for Automated Deduction (SAD): a tool for proof verification (2007)International Conference on Automated Deductionpages 398--403editor Pfenning, Frankorganization Springerdoi 10.1007/978-3-540-73595-3_29https://doi.org/10.1007/978-3-540-73595-3_29
  • [VLPA08]Verchinine, Konstantin; Lyaletski, Alexander; Paskevich, Andrei; Anisimov, AnatolyOn correctness of mathematical texts from a logical and practical point of view (2008)International Conference on Intelligent Computer Mathematicspages 583--598editors Autexier, Serge; Campbell, John A.; Rubio, Julio; et al.organization Springerdoi 10.1007/978-3-540-85110-3_47https://doi.org/10.1007/978-3-540-85110-3_47
  • [VSP+17]Vaswani, Ashish; Shazeer, Noam; Parmar, Niki; Uszkoreit, Jakob; Jones, Llion; Gomez, Aidan N.; Kaiser, Lukasz; Polosukhin, IlliaAttention is All you Need (2017)Neural Information Processing Systemspages 5998--6008editors Guyon, Isabelle; von Luxburg, Ulrike; Bengio, Samy; et al.https://proceedings.neurips.cc/paper/2017/hash/3f5ee243547dee91fbd053c1c4a845aa-Abstract.html
  • [Wad03]Wadler, PhilipA prettier printer (2003)The Fun of Programming, Cornerstones of Computingpages 223--243editors Gibbons, Jeremy; de Moor, Oegepublisher Palgrave MacMillanhttp://www.cs.ox.ac.uk/publications/books/fop
  • [Wen12]Wenzel, MakariusIsabelle/jEdit-A Prover IDE within the PIDE Framework. (2012)Intelligent Computer Mathematics - 11th International Conferencevolume 7362pages 468--471editors Jeuring, Johan; Campbell, John A.; Carette, Jacques; et al.publisher Springerdoi 10.1007/978-3-642-31374-5_38https://doi.org/10.1007/978-3-642-31374-5_38
  • [Wen18]Wenzel, MakariusIsabelle/PIDE after 10 years of development (2018)UITP workshop: User Interfaces for Theorem Provers. https://sketis.net/wp-content/uploads/2018/08/isabellepide-uitp2018.pdf
  • [Wen99]Wenzel, MarkusIsar - A Generic Interpretative Approach to Readable Formal Proof Documents (1999)Theorem Proving in Higher Order Logicsvolume 1690pages 167--184editors Bertot, Yves; Dowek, Gilles; Hirschowitz, André; et al.publisher Springerdoi 10.1007/3-540-48256-3_12https://doi.org/10.1007/3-540-48256-3_12
  • [Wie00]Wiedijk, FreekThe de Bruijn Factor (2000)http://www.cs.ru.nl/F.Wiedijk/factor/factor.pdf
  • [Wie07]Wiedijk, FreekThe QED manifesto revisited (2007)Studies in Logic, Grammar and Rhetoricvolume 10number 23pages 121--133http://www.cs.ru.nl/~freek/pubs/qed2.pdf
  • [Zha16]Zhan, BohuaAUTO2, a saturation-based heuristic prover for higher-order logic (2016)International Conference on Interactive Theorem Provingpages 441--456editors Blanchette, Jasmin Christian; Merz, Stephanorganization Springerdoi 10.1007/978-3-319-43144-4_27https://doi.org/10.1007/978-3-319-43144-4_27
  • [deB72]de Bruijn, Nicolaas GovertLambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972)Indagationes Mathematicae (Proceedings)volume 75number 5pages 381--392organization North-Hollandhttp://alexandria.tue.nl/repository/freearticles/597619.pdf
© 2021 E.W.Ayers. Built with Gatsby