@phdthesis(awodey97logicin,
 author       = "Steven Awodey",
 year         = "1997",
 title        = "Logic in topoi: Functorial Semantics for Higher-Order Logic",
 school       = "The University of Chicago",
)
@book(bridges1987varieties,
 author       = "Douglas Bridges and Fred Richman",
 year         = "1987",
 title        = "Varieties of Constructive Mathematics",
 series       = "Lecture note series",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/cbo9780511565663",
)
@article(curvesprufer,
 author       = "Thierry Coquand and Henri Lombardi and Claude Quitt{\'e}",
 year         = "2010",
 title        = "Curves and coherent Pr{\"u}fer rings",
 journal      = "J. Symb. Comput.",
 volume       = "45",
 number       = "12",
 pages        = "1378--1390",
 doi          = "10.1016/j.jsc.2010.06.016",
)
@article(Coste2001203,
 author       = "Michel Coste and Henri Lombardi and Marie-Fran\c {c}oise Roy",
 year         = "2001",
 title        = "Dynamical method in algebra: effective Nullstellens\"atze",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "111",
 number       = "3",
 pages        = "203 -- 256",
 doi          = "10.1016/S0168-0072(01)00026-4",
)
@incollection(duval0,
 author       = "Jean Della Dora and Claire Dicrescenzo and Dominique Duval",
 year         = "1985",
 title        = "About a new method for computing in algebraic number fields",
 editor       = "Bob Caviness",
 booktitle    = "EUROCAL '85",
 series       = "Lecture Notes in Computer Science",
 volume       = "204",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "289--290",
 doi          = "10.1007/3-540-15984-3\_279",
)
@article(Frohlich26011956,
 author       = "A. Fr{\"o}hlich and J. C. Shepherdson",
 year         = "1956",
 title        = "Effective Procedures in Field Theory",
 journal      = "Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences",
 volume       = "248",
 number       = "950",
 pages        = "407--432",
 doi          = "10.1098/rsta.1956.0003",
)
@book(elephant2,
 author       = "Peter T. Johnstone",
 year         = "2002",
 title        = "Sketches of an Elephant: A Topos Theory Compendium - Volume 2",
 series       = "Oxford Logic Guides",
 volume       = "44",
 publisher    = "Oxford University Press",
)
@article(Kennison19827,
 author       = "John F. Kennison",
 year         = "1982",
 title        = "Separable algebraic closure in a topos",
 journal      = "Journal of Pure and Applied Algebra",
 volume       = "24",
 number       = "1",
 pages        = "7 -- 24",
 doi          = "10.1016/0022-4049(82)90055-X",
)
@book(lombardi_book,
 author       = "Henri Lombardi and Claude Quitt{\'e}",
 year         = "2011",
 title        = "Alg{\`e}bre Commutative, M{\'e}thodes Constructives",
 series       = "Math{\'e}matiques en devenir",
 publisher    = "Calvage et Mounet",
)
@book(sheavesgeometry,
 author       = "Saunders MacLane and Ieke Moerdijk",
 year         = "1992",
 title        = "{Sheaves in Geometry and Logic: A First Introduction to Topos Theory}",
 edition      = "corrected",
 publisher    = "Springer",
 doi          = "10.1007/978-1-4612-0927-0",
)
@book(makkai1977first,
 author       = "Michael Makkai and Gonzalo E. Reyes",
 year         = "1977",
 title        = "First order categorical logic: model-theoretical methods in the theory of topoi and related categories",
 series       = "Lecture notes in mathematics",
 volume       = "611",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/BFb0066201",
)
@article(dynnewton,
 author       = "Bassel Mannaa and Thierry Coquand",
 year         = "2013",
 title        = "Dynamic Newton-Puiseux theorem",
 journal      = "J. Logic {\&} Analysis",
 volume       = "5",
 doi          = "10.4115/jla.2013.5.5",
)
@unpublished(martinloftypes,
 author       = "Per Martin-L{\"o}f",
 year         = "1972",
 title        = "An intuitionistic theory of types",
 note         = "Reprinted in Twenty-five years of constructive type theory, Oxford University Press, 1998, 127--172",
)
@book(Mines,
 author       = "Ray Mines and Fred Richman and Wim Ruitenburg",
 year         = "1988",
 title        = "A course in constructive algebra",
 series       = "Universitext (1979)",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/978-1-4419-8640-5",
)
@book(scedrov1984forcing,
 author       = "Andrej {\v {S}}{\v {c}}edrov",
 year         = "1984",
 title        = "Forcing and classifying topoi",
 series       = "Memoirs of the AMS",
 volume       = "48",
 publisher    = "American Mathematical Society (AMS)",
 doi          = "10.1090/memo/0295",
)