lean.bib

@InProceedings{lean-tactics,
 author = {Ebner, Gabriel and Ullrich, Sebastian and Roesch, Jared and Avigad, Jeremy and de Moura, Leonardo},
 title = {A metaprogramming framework for formal verification},
 year = {2017},
 issue_date = {August 2017},
 publisher = {ACM},
 % url = {https://doi.org/10.1145/3110278},
 doi = {10.1145/3110278},
 booktitle = {ICFP 2017},
 series = {PACMPL},
 number = {1, ICFP},
 month = aug,
 articleno = {Article 34},
 numpages = {29},
 keywords = {dependent type theory, theorem proving, metaprogramming, tactic language}
}

@InProceedings{lean-prover,
author="de Moura, Leonardo
and Kong, Soonho
and Avigad, Jeremy
and van Doorn, Floris
and von Raumer, Jakob",
editor="Felty, A. P.
and Middeldorp, A.",
title="The Lean theorem prover (system description)",
booktitle="Automated Deduction - CADE-25",
series="LNCS",
volume="9195",
year="2015",
publisher="Springer, Cham",
pages="378--388",
doi = {10.1007/978-3-319-21401-6_26},
}

@inproceedings{mathlib,
author = {{The mathlib Community}},
editor={Blanchette, J. and Hrițcu, C.},
title = {The Lean Mathematical Library},
year = {2020},
isbn = {9781450370974},
publisher = {ACM},
doi = {10.1145/3372885.3373824},
booktitle = {CPP 2020},
pages = {367–381},
numpages = {15},
keywords = {formal library, mathlib, formal proof, Lean},
}

@InProceedings{ring-tactic,
author="Gr{\'e}goire, Benjamin
and Mahboubi, Assia",
editor="Hurd, J.
and Melham, T.",
title="Proving equalities in a commutative ring done right in Coq",
booktitle="TPHOLs 2005",
year="2005",
series="LNCS",
volume="3603",
publisher="Springer, Berlin, Heidelberg",
pages="98--113",
abstract="We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation.",
doi = {10.1007/11541868_7},
}

@misc{norm-cast,
	title={Arithmetic and Casting in Lean},
	author={Paul-Nicolas Madelaine},
	year={2019},
	institution={Vrije Universiteit Amsterdam},
	note={MSc internship report},
}

@inproceedings{monad-transformers,
	author = {Liang, Sheng and Hudak, Paul and Jones, Mark},
	title = {Monad transformers and modular interpreters},
	series = {POPL '95},
	year = {1995},
	pages = {333--343},
	numpages = {11},
	% url = {http://doi.acm.org/10.1145/199448.199528},
	doi = {10.1145/199448.199528},
	acmid = {199528},
	publisher = {ACM},
}

@inproceedings{coq-lattices,
author = {James, Daniel and Hinze, Ralf},
year = {2009},
month = {06},
day = {2-4},
numpages = {11},
title = {A reflection-based proof tactic for lattices in Coq},
booktitle = {Post-conference proceedings of the 10th Symposium on Trends in Functional Programming},
location = {Komarno, Slovakia},
publisher={Intellect},
series={TFP 2009},
}

@inproceedings{coq-assoc-comm,
 author = {Braibant, Thomas and Pous, Damien},
 title = {Tactics for Reasoning modulo AC in Coq},
 year = {2011},
 isbn = {9783642253782},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 doi = {10.1007/978-3-642-25379-9_14},
 booktitle = {Proceedings of the First International Conference on Certified Programs and Proofs},
 pages = {167–182},
 numpages = {16},
 location = {Kenting, Taiwan},
 series = {CPP’11}
}

@InProceedings{resolution-rcf,
author="Akbarpour, Behzad
and Paulson, Lawrence C.",
editor="Dershowitz, Nachum
and Voronkov, Andrei",
title="Extending a resolution prover for inequalities on elementary functions",
booktitle="LPAR 2007",
series="LNCS",
volume="4790",
year="2007",
publisher="Springer, Berlin, Heidelberg",
pages="47--61",
abstract="Experiments show that many inequalities involving exponentials and logarithms can be proved automatically by combining a resolution theorem prover with a decision procedure for the theory of real closed fields (RCF). The method should be applicable to any functions for which polynomial upper and lower bounds are known. Most bounds only hold for specific argument ranges, but resolution can automatically perform the necessary case analyses. The system consists of a superposition prover (Metis) combined with John Harrison's RCF solver and a small amount of code to simplify literals with respect to the RCF theory.",
isbn="978-3-540-75560-9",
doi={10.1007/978-3-540-75560-9_6},
}

@InProceedings{hol_light,
author="Harrison, John",
editor="Srivas, Mandayam
and Camilleri, Albert",
title="HOL Light: A tutorial introduction",
booktitle="FMCAD 1996",
year="1996",
series="LNCS",
volume="1166",
publisher="Springer Berlin Heidelberg",
pages="265--269",
abstract="HOL Light is a new version of the HOL theorem prover. While retaining the reliability and programmability of earlier versions, it is more elegant, lightweight, powerful and automatic; it will be the basis for the Cambridge component of the HOL-2000 initiative to develop the next generation of HOL theorem provers. HOL Light is written in CAML Light, and so will run well even on small machines, e.g. PCs and Macintoshes with a few megabytes of RAM. This is in stark contrast to the resource-hungry systems which are the norm in this field, other versions of HOL included. Among the new features of this version axe a powerful simplifier, effective first order automation, simple higher-order matching and very general support for inductive and recursive definitions.",
isbn="978-3-540-49567-3",
	doi = {10.1007/BFb0031814},
}

@book{isabelle_hol,
editor="Nipkow, Tobias
and Wenzel, Markus
and Paulson, Lawrence C.",
title="Isabelle/HOL: A Proof Assistant for Higher-Order Logic",
year="2002",
publisher="Springer, Berlin, Heidelberg",
abstract="This book is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and verification system. Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for HOL,which abbreviates Higher-Order Logic. We introduce HOL step by step following the equation HOL = Functional Programming+ Logic.",
isbn="978-3-540-45949-1",
doi="10.1007/3-540-45949-9",
}

@InProceedings{reflection-tactics,
author="Boutin, Samuel",
editor="Abadi, Mart{\'i}n
and Ito, Takayasu",
title="Using reflection to build efficient and certified decision procedures",
booktitle="TACS 1997",
series="LNCS",
volume="1281",
year="1997",
publisher="Springer, Berlin, Heidelberg",
pages="515--529",
abstract="In this paper we explain how computational reflection can help build efficient certified decision procedure in reduction systems. We have developed a decision procedure on abelian rings in the Coq system but the approach we describe applies to all reduction systems that allow the definition of concrete types (or datatypes). We show that computational reflection is more efficient than an LCF-like approach to implement decision procedures in a reduction system. We discuss the concept of total reflection, which we have investigated in Coq using two facts: the extraction process available in Coq and the fact that the implementation language of the Coq system can be considered as a sublanguage of Coq. Total reflection is not yet implemented in Coq but we can test its performance as the extraction process is effective. Both reflection and total reflection are conservative extensions of the reduction system in which they are used. We also discuss performance and related approaches. In the paper,we assume basic knowledges of ML and proof-checkers.",
isbn="978-3-540-69530-1",
	doi = {10.1007/11541868_7},
}

@online{agda-stdlib,
	title={Agda standard library},
	author = {{The Agda Team}},
	url = {https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary},
	note = {version 1.3 for Agda 2.6.1},
}