patch

books/bookvolbib add references

Goal: Proving Axiom Sane

\begin{chunk}{axiom.bib}
@misc{Wiki19,
  author = "Wikipedia",
  title = {{Algebraic data type}},
  year = "2019",
  link = "\url{https://en.wikipedia.org/wiki/Algebraic_data_type}"
}

\end{chunk}

\index{MacKenzei, Donald}
\begin{chunk}{axiom.bib}
@book{Mack01,
  author = "MacKenzei, Donald",
  title = {{Mechanizing Proof: Computing, Risk, and Trust}},
  year = "2001",
  publisher = "MIT Press",
  isbn = "0-262-13393-8",
  keywords = "shelf"
}

\end{chunk}

\index{Selsam, Daniel}
\index{Ullrich, Sebastian}
\index{de Moura, Leonardo}
\begin{chunk}{axiom.bib}
@misc{Sels20,
  author = "Selsam, Daniel and Ullrich, Sebastian and 
            de Moura, Leonardo",
  title = {{Tabled Typeclass Resolution}},
  year = "2020",
  link = "\url{https://www.dropbox.com/s/5nxklkxvdh7xna9/typeclass.pdf}",
  comment = "preprint",
  abstract =
    "Typeclasses have proven an elegant and effective way of managing
    ad-hoc polymorphism in both programming languages and interactive
    proof assistants. However, the increasingly sophisticated uses of
    typeclasses within proof assistants has exposed two critical
    problems with existing typeclass resolution procedures: the 
    {\sl diamond problem} which causes exponential running times in
    both theory and practice, and the {\sl cycle problem}, which
    cuases loops in the presense of cycles and so thwarts many desired
    uses of typeclasses. We present a new typeclass resolution
    procedure, called {\sl tabled typeclass resolution}, that solve
    these problems. We have implemented our procedure for the upcoming
    version (v4) of the Lean Theorem Prover, and confirm empirically
    that it provides exponential speedups compared to all existing
    procedures in the presense of diamonds. Our procedure is
    sufficiently lightweight that it could easily be implemented in
    other systems. We hope our new procedure facilitates even more
    sophisticated uses of typeclasses in both software development and
    interactive theorem proving.",
  paper = "Sels20.pdf"
}

\end{chunk}

\index{Hoare, Tony}
\begin{chunk}{axiom.bib}
@article{Hoar03,
  author = "Hoare, Tony",
  title = {{The Verifying Compiler: A Grand Challenge for Computing
            Research}},
  journal = "Journal of the ACM",
  volume = "50",
  number = "1",
  pages = "63-69",
  year = "2003",
  abstract = 
    "This contribution proposes a set of criteria that distinguish a
    grand challenge in science or engineering from the many other
    kinds of short-term or long-term research problems that engage the
    interest of scientists and engineers. As an example drawn from
    Computer Science, it revives an old challenge: the contruction and
    application of a verifying compiler that guarantees correctness of
    a program before running it.",
  paper = "Hoar03.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen04,
  author = "Pfenning, Frank",
  title = {{Automated Theorem Proving}},
  year = "2004",
  link = "\url{https://www.cs.cmu.edu/~fp/courses/atp/handouts/atp.pdf}",
  paper = "Pfen04.pdf"
}

\end{chunk}

\index{Horgan, John}
\begin{chunk}{axiom.bib}
@misc{Horg93,
  author = "Horgan, John",
  title = {{The Death of Proof}},
  year = "1993",
  publisher = "Scientific American",
  paper = "Horg93.pdf"
}

\end{chunk}

\index{Licata, Dan}
\begin{chunk}{axiom.bib}
@misc{Lica16,
  author = "Licata, Dan",
  title = {{A Functional Programmer's Guide to Homotopy Type Theory}},
  year = "2016",
  comment = "ICFP conference",
  link = "\url{https://www.youtube.com/watch?v=caSOTjr1z18}"
}

\end{chunk}

\index{Licata, Dan}
\begin{chunk}{axiom.bib}
@misc{Lica16a,
  author = "Licata, Dan",
  title = {{Computing with Univalence}},
  year = "2016",
  comment = "Institute for Advanced Study",
  link = "\url{https://www.youtube.com/watch?v=YDdDuq2AGw4}"
}

\end{chunk}

\index{Pittman, Dan}
\begin{chunk}{axiom.bib}
@misc{Pitt18,
  author = "Pittman, Dan",
  title = {{Proof Theory Impressionism: Blurring the Curry-Howard Line}},
  year = "2018",
  comment = "StrangeLoop 2018",
  link = "\url{https://www.youtube.com/watch?v=jrVPB-Ad5Gc}"
}

\end{chunk}

\index{Baker, Henry G.}
\begin{chunk}{axiom.bib}
@misc{Bake93a,
  author = "Baker, Henry G.",
  title = {{Linear Logic and Permutation Stacks -- The Forth Shall Be First}},
  year = "1993",
  link = "\url{http:/home.pipeline.com/~hbaker1/ForthStack.html}",
  abstract =
    "Girard's linear logic can be used to model programming languages
    in which each bound variable name has exactly one ``occurence'' --
    i.e., no variable can have implicit ``fan-out'', multiple uses
    require explicit duplication. Among other nice properties,
    ``linear'' languages need no garbage collector, yet have no
    dangling reference problems. We show a natural equivalence between
    a ``linear'' programming language and a stack machine in which the
    top items can undergo arbitrary permutations. Such permutation
    stack machines can be considered combinator abstractions of
    Moore's {\sl Forth} programming language.",
  keywords = "DONE"
}

\end{chunk}

\index{Dijkstra, Edsger W.}
\begin{chunk}{axiom.bib}
@misc{Dijk78,
  author = "Dijkstra, Edsger W.",
  title = {{A Political Pamphlet From The Middle Ages}},
  year = "1978",
  comment = "EWD638",
  link = "\url{https://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD638.html}"
}

\end{chunk}

\index{Bridges, Douglas}
\index{Reeves, Steve}
\begin{chunk}{axiom.bib}
@article{Brid99,
  author = "Bridges, Douglas and Reeves, Steve",
  title = {{Constructive Mathematics in Theory and Programming
           Practice}}, 
  journal = "Philosophia Mathematica",
  volume = "7",
  number = "3",
  year = "1999",
  pages = "65-104",
  paper = "Brid99.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Pearce, David J.}
\index{Groves, Lindsay}
\begin{chunk}{axiom.bib}
@misc{Pear15,
  author = "Pearce, David J. and Groves, Lindsay",
  title = {{Designing a Verifying Compiler: Lessons Learned from
            developing Whiley}},
  year = "2015",
  link = "\url{https://homepages.ecs.vuw.ac.nz/~djp/files/SCP15-preprint.pdf}",
  abstract =
    "An ongoing challenge for computer science is the development of a
    tool which automatically verifies programms meet their
    specifications, and are free from runtime errors such as
    divide-by-zero, array out-of-bounds and null dereferences. Several
    impressive systems have been developed to this end, such as
    ESC/Java and Spec\#, which build on existing programming languages
    (e.g., Java, C\#). We have been developing a programming language
    from scratch to simplify verification, called Whiley, and an
    accompanying verifying compiler. In this paper, we present a
    technical overview of the verifying compiler and document the
    numerous design decisions made. Indeed, many of our designs
    reflect thos of similar tools. However, they have often been
    ignored in the literature and/or spread thinly throughout. In
    doing this, we hope to provide a useful resource for those
    building verifying compilers.",
  paper = "Pear15.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Rucker, Rudy}
\begin{chunk}{axiom.bib}
@book{Ruck87,
  author = "Rucker, Rudy",
  title = {{Mathenauts: Tales of Mathematical Wonder}},
  year = "1987",
  comment = "Norman Kagan: Four Brands of Impossible",
  publisher = "Arbor House Publishing"
}

\end{chunk}

\index{Woodcock, Jim}
\index{Davies, Jim}
@book{Wood20,
  author = "Woodcock, Jim and Davies, Jim"l
  title = {{Using Z: Specification, Refinement, and Proof}}
  year = "2020",
  link = "\url{http://www.cs.cmu.edu/~15819/zedbook.pdf}",
  publisher = "CMU PDF",
  paper = "Wood20.pdf"
}

\end{chunk}

\index{Chang, Stephen}
\index{Ballantyne, Michael}
\index{Turner, Milo}
\index{Bowman, William J.}
\begin{chunk}{axiom.bib}
@article{Chan20,
  author = "Chang, Stephen and Ballantyne, Michael and Turner, Milo
            and Bowman, William J.",
  title = {{Dependent Type Systems as Macros}},
  journal = "Proc. ACM Program Lang.",
  volume = "4",
  year = "2020",
  abstract =
    "We present {\tt TURNSTYLE+}, a high-level, macros-based metaDSL
    for building dependently typed languages. With it, programmers may
    rapidly prototype and iterate on the design of new dependently
    typed features and extensions. Or they may create entirely new
    DSLs whose dependet type ``power'' is tailored to a specific
    domain. Our framework's support of language-oriented programming
    also makes it suitable for experimenting with systems of
    interacting components, e.g. a proof assistant and its companion
    DSLs. This paper explains the implementation details of 
    {\tt TURNSTYLE+}, as well as how it may be used to create a wide
    variety of dependently typed languages, from a lightweight one
    with indexed types, to a full spectrum proof assistant, complete
    with a tactic system and extensions for features like sized types
    and SMT interaction.",
  paper = "Chan20.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Warne, Henrik}
\begin{chunk}{axiom.bib}
@misc{Warn19,
  author = "Warne, Henrik",
  title = {{More Good Programming Quotes, Part 3}},
  year = "2019",
  link = "\url{https://henrikwarne.com/2019/04/03/more-good-programming-quotes-part-3}"
}

\end{chunk}

\index{Warne, Henrik}
\begin{chunk}{axiom.bib}
@misc{Warn16,
  author = "Warne, Henrik",
  title = {{More Good Programming Quotes}},
  year = "2019",
  link = "\url{https://henrikwarne.com/2016/04/17/more-good-programming-quotes}"
}

\end{chunk}

\index{Baccala, Brent W.}
\begin{chunk}{axiom.bib}
@misc{Bacc,
  author = "Baccala, Brent W.",
  title = {{The Facebook Integral}},
  year = "2020",
  link = "\url{https://ec2.freesoft.org/blogs/soapbox/the-facebook-integral}"
}

\end{chunk}

\index{Baccala, Brent W.}
\begin{chunk}{axiom.bib}
@misc{Bacca,
  author = "Baccala, Brent W.",
  title = {{The Facebook Integral (solved with Axiom and Sage}},
  year = "2020",
  link = "\url{https://youtu.be/tz1LwfJlMuo}"
}

\end{chunk}

\index{Baccala, Brent W.}
\begin{chunk}{axiom.bib}
@misc{Baccb,
  author = "Baccala, Brent W.",
  title = {{The Risch Theorem}},
  year = "2020",
  link = "\url{https://youtu.be/BGnLwhXb204}"
}

\end{chunk}

\index{Goel, Shilpi}
\index{Slobodova, Anna}
\index{Sumners, Rob}
\index{Swords, Sol}
\begin{chunk}{axiom.bib}
@misc{Goel19,
  author = "Goel, Shilpi and Slobodova, Anna and Sumners, Rob and
            Swords, Sol",
  title = {{Verifying X86 Instruction Implementations}},
  year = "2019",
  link = "\url{https://arxiv.org/abs/1912.10285}",
  paper = "Goel19.pdf"
}

\end{chunk}

\index{Boizumault, Patrice}
\index{Djamboulian, Ara M.}
\index{Fattouh, Jamal}
\begin{chunk}{axiom.bib}
@book{Boiz93,
  author = "Boizumault, Patrice and Djamboulian, Ara M. and Fattouh, Jamal",
  title = {{The Implementation of Prolog}}
  year = "1993",
  publisher = "Princeton Legacy Library",
  keywords = "shelf"
}

\end{chunk}

\index{Clark, K.L.}
\index{McCabe, F.G.}
\begin{chunk}{axiom.bib}
@book{Clar84,
  author = "Clark, K.L. and McCabe, F.G.",
  title = {{micro-PROLOG: Programming in Logic}},
  year = "1984",
  publisher = "Prentice-Hall",
  isbn = "0-13-581264-X",
  keywords = "shelf"
}

\end{chunk}

\index{Abelson, Harold}
\index{Sussman, Gerald Jay}
\index{Sussman, Julie}
\begin{chunk}{axiom.bib}
@book{Abel86,
  author = "Abelson, Harold and Sussman, Gerald Jay and Sussman, Julie", 
  title = {{Structure and Interpretation of Computer Programs}},
  year = "1986",
  publisher = "The MIT Press",
  isbn = "0-262-01077-1",
  keywords = "shelf"
}

\end{chunk}

\index{Chandy, K. Mani}
\index{Misra, Jayadev}
\begin{chunk}{axiom.bib}
@book{Chan89,
  author = "Chandy, K. Mani and Misra, Jayadev",
  title = {{Parallel Program Design}},
  year = "1989",
  publisher = "Addison-Wesley Publishing",
  isbn = "0-201-05866-9",
  keywords = "shelf"
}

\end{chunk}

\index{Bundy, Alan}
\begin{chunk}{axiom.bib}
@book{Bund83,
  author = "Bundy, Alan",
  title = {{The Computer Modelling of Mathematics Reasoning}},
  year = "1983",
  publisher = "Academic Press",
  isbn = "0-12-141250-4",
  keywords = "shelf"
}

\end{chunk}

\index{Hamilton, A.G.}
\begin{chunk}{axiom.bib}
@book{Hami78,
  author = "Hamilton, A.G.",
  title = {{Logic for Mathematicians}},
  year = "1978",
  publisher = "Cambridge University Press",
  isbn = "0-521-29291-3",
  keywords = "shelf"
}

\end{chunk}

\index{Michaelson, S.}
\index{Milner, R.}
\begin{chunk}{axiom.bib}
@book{Mich76,
  author = "Michaelson, S. and Milner, R.",
  title = {{Automata Languages and Programming}},
  year = "1976",
  publisher = "Edinburgh University Press",
  isbn = "0-85224-308-1",
  keywords = "shelf"
}

\end{chunk}

\index{Campbell, J.A.}
\begin{chunk}{axiom.bib}
@book{Camp84,
  author = "Campbell, J.A.",
  title = {{Implementations of PROLOG}},
  year = "1984",
  publisher = "Ellis Horwood Limited",
  isbn = "0-85312-675-5",
  keywords = "shelf"
}

\end{chunk}

\index{Reichenbach, Hans}
\begin{chunk}{axiom.bib}
@book{Reic47,
  author = "Reichenbach, Hans",
  title = {{Elements of Symbolic Logic}},
  year = "1947",
  publisher = "The MacMillan Company",
  keywords = "shelf"
}

\end{chunk}

\index{Oesterle, John A.}
\begin{chunk}{axiom.bib}
@book{Oest53
  author = "Oesterle, John A.",
  title = {{Logic: The Art of Defining and Reasoning}},
  year = "1953",
  publisher = "Prentice-Hall",
  keywords = "shelf"
}

\end{chunk}

\index{Lewis, Robert Y.}
\index{Wu, Minchao}
\begin{chunk}{axiom.bib}
@misc{Lewi17,
  author = "Lewis, Robert Y. and Wu, Minchao",
  title = {{A Bi-directional extensible ad hoc interface between Lean
            and Mathematica}},
  year = "2017",
  link = "\url{https://robertylewis.com/leanmm/lean_mm.pdf}",
  abstract =
    "We implement a user-extensible ad hoc connection between the Lean
    proof assistant and the computer algebra system Mathematica. By
    reflecting the syntax of each system in the other and providing a
    flexible interface for extending translation, our connection
    allows for the exchange of arbitrary information between the two
    systemss. We show how to make use of the Lean metaprogramming
    framework to verif certain Mathematica computations, so that the
    rigor of the proof assistant is not compromised. We also establish
    a connection in the opposite direction, using Mathematica to
    import and process proof terms from Lean.",
  paper = "Lewi17.pdf",
  keywords = "printed"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Unkn20,
  author = "Unknown",
  title = {{Programming is Terrible -- Lessons Learned from a life
            wasted}}, 
  year = "2020",
  link = "\url{https://programmingisterrible.com/post/65781074112/devils-dictionary-of-programming}"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Comm16,
  author = "Unknown",
  title = {{A very comprehensive and precise spec}},
  year = "2016"
  link =
  "\url{http://www.commitstrip.com/en/2016/08/25/a-very-comprehensive-and-precise-spec}"
}

\end{chunk}

\index{Pfenning, Frank}
\index{Schurmann, Carston}
\begin{chunk}{axiom.bib}
@misc{Pfen99,
  author = "Pfenning, Frank and Schurmann, Carston",
  title = {{System Description: Twelf -- A Meta-Logical Framework for
            Deductive Systems}},
  year = "1999",
  link = "\url{https://www.cs.cmu.edu/~fp/papers/cade99.pdf}",
  abstract =
    "Twelf is a meta-logical framework for the specification,
    implementation, and meta-theory of deductive systems from the
    theory of programming languages and logics. It relies on the LF
    type theory and the jugements-as-types methodology for
    specifications [HHP93], a constraint logic programming interpreter
    for implementation [Pfe91], and the meta-logic $M_2$ for reasoning
    about object languages encoded in LF [SP98]. It is a significant
    extension and complete reimplementation of the Elf system [Pfe94]. 

    Twelf is written in Standard ML and runs under SML of New Jersey
    and MLWorks on Unix and Window platforms. The current version
    (1.2) is distributed with a complete manual, example suites, a
    tutorial in the form of on-line lecture notes [Pfe], and an Emacs
    interface. Source and binary distributions are accessible via the
    Twelf home page \url{http://www.cs.cmu.edu/~twelf}.",
  paper = "Pfen99.pdf",
  keywords = "printed"
}

\end{chunk}

\index{Pfenning, Frank}
\begin{chunk}{axiom.bib}
@misc{Pfen94,
  author = "Pfenning, Frank",
  title = {{Elf: A Meta-Language for Deductive Systems}},
  year = "1994",
  paper = "Pfen94.pdf",
  keywords = "printed, DONE"
}

\end{chunk}

\index{Thornton, Jacob}
\begin{chunk}{axiom.bib}
@misc{Thor12,
  author = "Thornton, Jacob",
  title = {{What is Open Source and Why Do I Feel So Guilty}},
  year = "2012",
  link = "\url{https://www.youtube.com/watch?v=UIDb6VBO9os}"
}

\end{chunk}

\index{Bazerman, Gershom}
\begin{chunk}{axiom.bib}
@misc{Baze14,
  author = "Bazerman, Gershom",
  title = {{Homotopy Type Theory: What's the Big Idea}},
  year = "2014",
  comment = "Lambda Jam 2014",
  link = "\url{https://www.youtube.com/watch?v=OupcXmLER7I}"
}

\end{chunk}

\index{Voevodsky, Vladimir}
\begin{chunk}{axiom.bib}
@misc{Voev10,
  author = "Voevodsky, Vladimir",
  title = {{The Equivalence Axiom and Univalent Models of Type
           Theory}},
  year = "2010",
  link = "\url{https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/CMU_talk.pdf}",
  abstract =
    "I will show how to define, in any type system with dependent
    sums, products and Martin-Lof identity types, the notion of a
    homotopy equivalence between two types and how to formulate the
    Equivalence Axiom which provides a natural way to assert that
    ``two homotopy equivalent types are equal''. I will then sketch a
    construction of a model of one of the standard Martin-Lof type
    theories which satisfies the equivalence axiom and the excluded
    middle thus proving that M.L. type theory with excluded middle and
    equivalence axiom is at least as consistent as ZFC theory.

    Models which satisfy the equivalence axiom are called
    univalent. This is a totally new class of models and I will argue
    that the semantics which they provide leads to the first
    satisfactory approach to type-theoretic formalization of
    mathematics.",
  paper = "Voev10.pdf",
  keywords = "printed"
}

\end{chunk}