proofsPrograms.bib

@Book{hottbook,
  author =    {The {Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address =   {Institute for Advanced Study},
  year =      2013}

@Inbook{naiveTT,
author="Altenkirch, Thorsten",
title="Na{\"i}ve Type Theory",
bookTitle="Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts",
year="2019",
publisher="Springer International Publishing",
url="www.cs.nott.ac.uk/~psztxa/publ/fomus19.pdf"
}

% Lambda Calculus and Type Theory
@book{curryCombinatoryLogic,
    title = {Combinatory Logic},
    author = {Haskell B. Curry, Robert Feys},
    year = {1958},
    publisher = {North-Holland Publishing Company, Amsterdam}
}
% First(?) sign of CH-Isomorphism given here in 6E.3
@book{pat,
    title = {Proofs and Types},
    author = {Jean-Yves Girard, Paul Taylor, and Yves Lafont},
    year = {1989},
    publisher = {Cambridge University Press}
}

@article{griffin ,
author = {Timothy G. Griffin},
title = {A Formulae-as-Types Notion of Control},
journal = {Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL},
year = {1990}
}

@incollection{Howard1980,
	author = {William Alvin Howard},
	booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism},
	year = {1980},
	publisher = {Academic Press},
	title = {The Formulae-as-Types Notion of Construction},
	editor = {Haskell Curry and Hindley B. and Seldin J. Roger and P. Jonathan}
}

@book{pierce,
    title = {Types and Programming Languages},
    author = {Benjamin C. Pierce},
    year = {2002},
    publisher = {The MIT Press. Cambridge, Massachusetts. London, England}
}

@book{logics,
    title = {Classical and Nonclassical Logics},
    author = {Eric Schechter},
    year = {2005},
    publisher = {Princeton University Press}
}

@book{thompson,
    title = {Type Theory and Functional Programming},
    author = {Simon Thompson},
    year = {1991},
    publisher = {Addison-Wesley Publishers Ltd.},
    keywords = {type-theory}
}

% Chapter 6 has stuff about classical logic and CHI. 
@book{LoCHI,
    title = {Studies in Logic and the Foundations of Mathematics: Lectures on the Curry-Howard Isomorphism},
    author = {M.H. S\o rensen and P. Urzyczyn},
    year = {2006},
	volume = {149},
    publisher = {Elsevier}
}

% Logic textbooks
@book{vDalen,
    title = {Logic and Structure},
    author = {Dirk van Dalen},
    year = {1980},
    publisher = {Springer-Verlag}
}

@book{goldblatt,
    title = {Topoi: The Categorical Analysis of Logic},
    author = {Robert Goldblatt},
    year = {1984},
    publisher = {North Holland}
}

@book{smithIntro,
    title = {An Introduction to Formal Logic},
    author = {Peter Smith},
    year = {2020},
    publisher = {Cambridge University Press},
    keywords = {logic}
}

% SEP articles
@InCollection{sep-mathematics-constructive,
	author       =	{Bridges, Douglas and Palmgren, Erik and Ishihara, Hajime},
	title        =	{{Constructive Mathematics}},
	booktitle    =	{The {Stanford} Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta and Uri Nodelman},
	howpublished =	{\url{https://plato.stanford.edu/archives/fall2022/entries/mathematics-constructive/}},
	year         =	{2022},
	edition      =	{{F}all 2022},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}

@InCollection{sep-intuitionism,
	author       =	{Iemhoff, Rosalie},
	title        =	{{Intuitionism in the Philosophy of Mathematics}},
	booktitle    =	{The {Stanford} Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{https://plato.stanford.edu/archives/fall2020/entries/intuitionism/}},
	year         =	{2020},
	edition      =	{{F}all 2020},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}

@InCollection{sep-type-theory,
	author       =	{Coquand, Thierry},
	title        =	{{Type Theory}},
	booktitle    =	{The {Stanford} Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta and Uri Nodelman},
	howpublished =	{\url{https://plato.stanford.edu/archives/fall2022/entries/type-theory/}},
	year         =	{2022},
	edition      =	{{F}all 2022},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}


% The following references were browsed for content 
% at the UC Central Library on July 4 2024. 

% Constructivism in Mathematics by Troelstra and van Dalen 
% Comes in two volumes. 

% Chapter 2 page 40 has rules of inference. 
% Chapter 2 page 47 has mention of "deductions from axioms". 
% Chapter 2 page 48 treats identity = as "mathematical" 
% Intuitionistic logic is referred to as IPC/IQC in its 
% propositional resp. first order variants. 
% Chapter 2 has interesting notes on Intuitionistic First Order 
% Arithmetic aka Heyting Arithmetic (HA)
% Volume 2 has chapters on Type Theory and Model Theory. 
% Model theory of Lattices and ** Heyting Algebras ** is the 
%   type I am interested in. 
% There are also notes on Categorial semantics. Sites etc. 
@book{constructivismInMath,
    title = {Constructivism in Mathematics: An Introduction},
    author = {Troelstra, A.S. and van Dalen, D},
    year = {1988},
    publisher = {North Holland},
    keywords = {logic}
}

% Chapter 1 Section 1 page 3:
%   Reference to non-standard model of arithmetic 
%   by Skolem in 1934 (post-Godel...)
% On page 4 the empty model is distinguished. Whereas page 20 
% (moved onto predicate logic) says models are to be nonempty. 
% Has same proof of completeness and soundess as van Dalen.
@book{changKeisler,
    title = {Model Theory},
    author = {Chang, C.C. and Keisler, H.J.},
    year = {1990},
    publisher = {North Holland}
}

% Awodey's book on category theory has explicit mention of 
% the lambda calculus and its relation to CCC. 

% This has excellent coverage of intuitionistic semantics
% Curry-Howard-LAMBEK
% Should be good for a student project. 
@book{awodey,
    title = {Category Theory},
    author = {Steve Awodey},
    year = {2010},
    publisher = {Oxford University Press}
}

% Classic!
@book{johnstoneTopos,
    title = {Topos Theory},
    author = {Johnstone, P.T.},
    year = {1977},
    publisher = {Acadmic Press}
}

% Another, classic!
@book{sheavesGaL,
    title = {Sheaves in Geometry and Logic},
    author = {Mac Lane, S and Moerdijk, I},
    year = {1992},
    publisher = {Springer}
}

% This book is explicit about the relationship between
% categories and types. It also mentions two others: 
%   Asperti and Longo: Categories Types and Structures. 
%   Pierce: Basic Category Theory for Computer Scientists.
@book{crole,
    title = {Categories for Types},
    author = {Crole, R.L.},
    year = {1993},
    publisher = {Cambridge University Press}
}

% Could be fun to translate the following book from ML 
% into Haskell. Make all constructions explicit in Haskell. 
@book{compCat,
    title = {Computational Category Theory},
    author = {Rydeheard, D.E. and Burstall, R.M.},
    year = {1988},
    publisher = {Prentice Hall}
}