lp:axiom
 Get this branch:
 bzr branch lp:axiom
Branch merges
Branch information
Import details
This branch is an import of the HEAD branch of the Git repository at git://github.com/daly/axiom.git.
Last successful import was .
Recent revisions
 2877. By daly on 20180630

books/bookvol10.1 add chapter on Primality Testing
Goal: Axiom Literate Programming
 2876. By daly on 20180630

books/bookvol13 add additional ideas to explore
Goal: Proving Axiom Sane
 2874. By daly on 20180630

books/bookvolbib add references
Goal: Proving Axiom Sane
\index{Davenport, James H.}
\begin{chunk}{ axiom.bib}
@article{Dave12b,
author = "Davenport, James H.",
title = {{Small Algorithms for Small Systems}},
journal = "ACM Comm. in Computer Algebra",
volume = "46",
number = "1",
year = "2012",
paper = "Dave12b.pdf"
}\end{chunk}
\index{Stoutemyer, David R.}
\begin{chunk}{ axiom.bib}
@article{Stou12,
author = "Stoutemyer, David R.",
title = {{Series Crimes}},
journal = "ACM Comm. in Computer Algebra",
volume = "46",
number = "2",
year = "2012",
abstract =
"Puiseux series are power series in which the exponents can be
fractional and/or negative rational numbers. Several computer algebra
systems have one or more builtin or loadable functions for computing
truncated Puiseux series. Some are generalized to allow coefficients
containing functions of the series variable that are dominated by any
power of that variable, such as logarithms and nested logarithms of
the series variable. Some computer algebra systems also have builtin
or loadable functions that compute infinite Puiseuxseries.
Unfortunately, there are some littleknown pitfalls in
computing Puiseux series. The most serious of these is expansions
within branch cuts or at branch points that are incorrect for some
directions in the complex plane. For example with each series
implementation accessible to you:Compare the value of $(z^2 + z^3)^{3/2}$ with that of its
truncated series expansion about $z = 0$, approximated at
$z = −0.01$. Does the series converge to a value that is
the negative of the correct value?Compare the value of $ln(z^2 + z^3)$ with its truncated series
expansion about $z = 0$, approximated at $z= −0.01 + 0.1i$. Does
the series converge to a value that is incorrect by $2\pi i$?Compare $arctanh(−2 + ln(z)z)$ with its truncated series
expansion about $z = 0$, approximated at $z = −0.01$. Does the series
converge to a value that is incorrect by about $\pi i$?At the time of this writing, most implementations that accommodate
such series exhibit such errors. This article describes how to avoid
these errors both for manual derivation of series and when
implementing series packages.",
paper = "Stou12.pdf"
}\end{chunk}
\index{Blair, Fred W.}
\index{Griesmer, James H.}
\index{Harry, Joseph}
\index{Pivovonsky, Mark}
\begin{chunk}{ axiom.bib}
@misc{Blai71,
author = "Blair, Fred W. and Griesmer, James H. and Harry, Joseph and
Pivovonsky , Mark",
title = {{Design and Development Document for Lisp on Several S/360
Operating Systems}},
year = "1971",
publisher = "IBM Research",
paper = "Blai71.pdf"
}\end{chunk}
\index{Alford, W.R.}
\index{Granville, A.}
\index{Pomerance, C.}
\begin{chunk}{ axiom.bib}
@misc{Alfo92,
author = "Alford, W.R. and Granville, A. and Pomerance, C.",
title = {{There are Infinitely Many Carmichael Numbers}},
year = "1992",
comment = "Preprint"
}\end{chunk}
\index{Arnault, F.}
\begin{chunk}{ axiom.bib}
@misc{Arna91,
author = "Arnault, F.",
title = {{Le Test de Primalite de RabinMiller: Un Nombre compose
qui le "passe"}},
comment = "Report 61",
university = "Universite de Poitiers Departement de Mathematiques",
year = "1991"
}\end{chunk}
\index{Damgard, I.}
\index{Landrock, P.}
\begin{chunk}{ axiom.bib}
@misc{Damg91,
author = "Damgard, I. and Landrock, P.",
title = {{Improved Bounds for the Rabin Primality Test}},
booktitle = "Proc. 3rd IMA Conf. on Coding and Cryptography",
year = "1991"
}\end{chunk}
\index{Davenport, James H.}
\index{Smith, G.C.}
\begin{chunk}{ axiom.bib}
@misc{Dave87,
author = "Davenport, James H. and Smith, G.C.",
title = {{Rabin's Primality Testing Algorithm  a Group Theory View}},
school = "University of Bath",
type = "technical report",
number = "8704",
year = "1987"
}\end{chunk}
\index{Jaeschke, G.}
\begin{chunk}{ axiom.bib}
@misc{Jaes91,
author = "Jaeschke, G.",
title = {{Private Communication}},
comment = "to James Davenport",
year = "1991"
}\end{chunk}
\index{Leech, J.}
\begin{chunk}{ axiom.bib}
@misc{Leec92,
author = "Leech, J.",
title = {{Private Communication}},
comment = "to James Davenport",
year = "1992"
}\end{chunk}
\index{Koblitz, N.}
\begin{chunk}{ axiom.bib}
@book{Kobl87,
author = "Koblitz, N.",
title = {{A Cource in Number Theory and Cryptography}},
publisher = "SpringerVerlog",
year = "1987"
}\end{chunk}
\index{Lenstra Jr., H.W.}
\begin{chunk}{ axiom.bib}
@article{Lens81,
author = "Lenstra Jr., H.W.",
title = {{Primality Testing Algorithms}},
journal = "Lecture Notes in Mathematics",
volume = "901",
publisher = "SpringerVerlag",
pages = "243257",
year = "1981"
}\end{chunk}
\index{Pomerance, C.}
\index{Slefridge, J.L.}
\index{Wagstaff Jr., S.S.}
\begin{chunk}{ axiom.bib}
@article{Pome80,
author = "Pomerance, C. and Slefridge, J.L. and Wagstaff Jr., S.S.",
title = {{The Pseudoprimes up to $25\cdot 10^9$}},
journal = "Math. Comp.",
volume = "35",
pages = "10031026",
year = "1980"
}\end{chunk}
\index{Rabin, M.O.}
\begin{chunk}{ axiom.bib}
@article{Rabi80,
author = "Rabin, M.O.",
title = {{Probabilistic Algorithm for Testing Primality}},
journal = "J. Number Theory",
volume = "12",
pages = "128138",
year = "1980"
}\end{chunk}
\index{Steele, Guy Lewis}
\index{Sussman, Gerald Jay}
\begin{chunk}{ axiom.bib}
@techreport{Stee78a,
author = "Steele, Guy Lewis and Sussman, Gerald Jay",
title = {{The Art of the Interpreter}},
institution = "MIT",
type = "technical report",
number = "AI Memo No. 453",
year = "1978",
abstract =
"We examine the effes of various language design decisions on the
programming styles available to a user of the language, with
particular emphasis on the ability to incrementatlly construct
modular systems. At each step we exhibit an interactive
metacircular interpreter for the language under
consideration. Each new interpreter is the result of an
incremental change to the previous interpreter.We explore the consequences of various variable binding
disciplines and the introduction of side effects. We find that
dynamic scoping is unsuitable for constructing procedural
abstractions, but has another role as an agent of modularity,
being a structured form of side effect. More general side effects
are also found to be necessary to promote modular style. We find
that the notion of side effect and the notion of equality (object
identity) are mutually constraining; to define one is to define
the other.The interpreters we exhibit are all written in a simple dialect of
LISP, and all implement LISPlike languages. A subset of these
interpreters constitute a partial historical reconstruction of the
actual evolution of LISP."
}\end{chunk}
\index{Constable, Robert L.}
\begin{chunk}{ axiom.bib}
@incollection{Cons03,
author = "Constable, Robert L.",
title = {{Naive Computational Type Theory}},
booktitle = "Proof and System Reliability",
publisher = "unknown",
link = "\url{http://www.nuprl. }",org/documents/ Constable/ naive.pdf
year = "2003",
paper = "Cons03.pdf"
}\end{chunk}
\index{Waaldijk, Frank}
\begin{chunk}{ axiom.bib}
@misc{Waal03,
author = "Waaldijk, Frank",
title = {{On the Foundations of Constructive Mathematics}},
link = "\url{}",
year = "2003",
abstract =
"We discuss the foundations of constructive mathematics, including
recursive mathematics and intuitionism, in relation to classical
mathematics. There are connections with the foundations of physics,
due to the way in which the different branches of mathematics reflect
reality. Many different axioms and their interrelationship are
discussed. We show that there is a fundamental problem in bish
(Bishop’s school of constructive mathematics) with regard to its
current definition of ‘continuous function’. This problem is closely
related to the definition in bish of ‘locally compact’.Possible approaches to this problem are discussed. Topology seems to
be a key to understanding many issues. We offer several new
simplifying axioms, which can form bridges between the various
branches of constructive mathematics and classical mathematics
(‘reuniting the antipodes’). We give a simplification of basic
intuitionistic theory, especially with regard to socalled ‘bar
induction’. We then plead for a limited number of axiomatic systems,
which differentiate between the various branches of mathematics.
Finally, in the appendix we offer bish an elegant topological
definition of ‘locally compact’, which unlike the current definition
is equivalent to the usual classical and/or intuitionistic definition
in classical and intuitionistic mathematics respectively.",
paper = "Waal03.pdf"
}\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@article{Farm95b,
author = "Farmer, William M.",
title = {{Reasoning about Partial Functions with the Aid of a
Computer} },
journal = "Erkenntnis",
volume = "43",
number = "3",
pages = "279294",
year = "1995",
abstract =
"Partial functions are ubiquitous in both mathematics and computer
science. Therefore, it is imperative that the underlying logical
formalism for a generalpurpose mechanized mathematics system
provide strong support for reasoning about partial
functions. Unfortunately, the common logical formalisms 
firstorder logic, type theory, and set theory  are usually only
adequate for reasoning about partial functions {\sl in
theory}. However, the approach to partial functions traditionally
employed by mathematicians is quite adequate {\sl in
practice}. This paper shows how the traditional approach to
partial functions can be formalized in a range of formalisms that
includes firstorder logic, simple type theory, and VonNeuman,
Bernays, Godel set theory. It argues that these new formalisms
allow one to directly reason about partial functions; are based on
natural, wellunderstood, familiar principles; and can be
effectively implemented in mechanized mathematics systems.",
paper = "Farm95b.pdf",
keywords = "printed"
}\end{chunk}
\index{Fong, Brendan}
\index{Spivak, David I.}
\begin{chunk}{ axiom.bib}
@misc{Fong18,
author = "Fong, Brendan and Spivak, David I.",
title = {{Seven Sketches in Compositionality: An Invitation to
Applied Category Theory}},
link = "\url{http://math.mit. }",edu/~dspivak/ teaching/ sp18/7Sketches. pdf
year = "2018",
paper = "Fong18.pdf"
}\end{chunk}
\index{Popov, Nikolaj}
\begin{chunk}{ axiom.bib}
@misc{Popo03,
author = "Popov, Nikolaj",
title = {{Verification Using Weakest Precondition Strategy}},
comment = "Talk at Comp. Aided Verfication of Information Systems",
year = "2003",
location = "Timisoara, Romania",
abstract =
"We describe the weakest precondition strategy for verifying
programs. This is a method which takes a specification and an
annotated program and generates socalled verification conditions:
mathematical lemmata which have to be proved in order to obtain a
formal correctness proof for the program with respect to its
specification. There are rules for generating the intermediate pre
and post conditions algorithmically. Based on these rules, we have
developed a package for generating verification conditions.",
paper = "Popo03.pdf",
keywords = "printed"
}\end{chunk}
\index{Kovacs, Laura}
\index{Jebelean, Tudor}
\begin{chunk}{ axiom.bib}
@article{Kova04,
author = "Kovacs, Laura and Jebelean, Tudor",
title = {{Practical Aspects of Imperative Program Verification in
Theorema} },
journal = "Analele Universitatu din Timisoara",
volume = "XXXXIX",
number = "2",
year = "2004",
abstract =
"Approaching the problem of imperative program verification from a
practical point of view has certain implications concerning: the style
of specifications, the programming language which is used, the help
provided to the user for finding appropriate loop invariants, the
theoretical frame used for formal verification, the language used
for expressing generated verification theorems as well as the database
of necessary mathematical knowledge, and finally the proving power,
style and language. The Theorema system (www. theorema.org) has
certain capabilities which make it appropriate for such a practical
approach. Our approach to imperative program verification in Theorema
is based on Hoare– Logic and the Weakest Precondition Strategy. In
this paper we present some practical aspect of our work, as well as a
novel method for verification of pro grams that contain loops, namely
a method based on recurrence equation solvers for generating the
necessary loop invariants and termination terms automatically. We
have tested our system with numerous examples, some of these example
are presented at the end of the paper.",
paper = "Kova04.pdf",
keywords = "printed"
}\end{chunk}
\index{Kovacs, Laura}
\index{Jebelean, Tudor}
\begin{chunk}{ axiom.bib}
@article{Kova04a
author = "Kovacs, Laura and Jebelean, Tudor",
title = {{Automated Generation of Loop Invariants by Recurrence
Solving in Theorema}},
year = "2004",
abstract =
"Most of the properties established during program verification are
either invariants or depend crucially on invariants. The effectiveness
of automated verification of (imperative) programs is therefore
sensitive to the ease with which invariants, even trivial ones, can be
automatically deduced. We present a method for invariant generation
that relies on combinatorial techniques, namely on recurrence solving
and variable elimination. The effectiveness of the method is
demonstrated on examples.",
paper = "Kova04a.pdf",
keywords = "printed"
}\end{chunk}
\index{Kovacs, Laura}
\begin{chunk}{ axiom.bib}
@phdthesis{Kova07,
author = "Kovacs, Laura",
title = {{Automated Invariant Generation by Algebraic Techniques for
Imperative Program Verification in Theorema}},
school = "JohannesKepler University Linz",
year = "2007",
abstract ="This thesis presents algebraic and combinatorial approaches for
reasoning about imperative loops with assignments, sequencing and
conditionals.A certain family of loops, called Psolvable , is defined for which
the value of each program variable can be expressed as a polynomial of
the initial values of variables, the loop counter, and some new
variables where there are algebraic dependencies among the new
variables. For such loops, a systematic method is developed for
generating polynomial invariants. Further, if the bodies of these
loops consist only of assignments and conditional branches, and test
conditions in the loop and conditionals are ignored, the method is
shown to be complete for some special cases. By completeness we mean
that it generates a set of polynomials from which, under additional
assumptions for loops with conditional branches, any polynomial
invariant can be derived. Many nontrivial algorithms working on
numbers can be naturally implemented using Psolvable loops.By combining advanced techniques from algorithmic combinatorics,
symbolic summation, computer algebra and computational logic, a
framework is developed for generating polynomial invariants for
imperative programs operating on numbers.Exploiting the symbolic manipulation capabilities of the computer
algebra system Mathematica , these techniques are implemented in a new
software package called Aligator . By using several combinatorial
packages developed at RISC, Aligator includes algorithms for solving
special classes of recurrence relations (those that are either
Gospersummable or Cfinite) and generating polynomial dependencies
among algebraic exponential sequences. Using Aligator , a complete set
of polynomial invariants is successfully generated for numerous
imperative programs working on numbers.The automatically obtained invariant assertions are subsequently used
for proving the partial correctness of programs by generating
appropriate verification conditions as firstorder logical formulas.
Based on Hoare logic and the weakest precondition strategy, this
verification process is supported in an imperative verification
environment implemented in the Theorema system. Theorema is
convenient for such an integration given that it is built on top of
the computer algebra system Mathematica and includes automated methods
for theorem proving in predicate logic, domain specific reasoning and
proving by induction.",
paper = "Kova07.pdf"
}\end{chunk}
\index{Kovacs, Laura}
\begin{chunk}{ axiom.bib}
@inproceedings{Kova08,
author = "Kovacs, Laura",
title = {{Reasoning Algebraiclly About PSolvable Loops}},
booktitle = "Int. Conf. on Tools and Algorithms for the Construction
and Analysis of Systems",
pages = "249264",
year = "2008",
abstract =
"We present a method for generating polynomial invariants for a
subfamily of imperative loops operating on numbers, called the
Psolvable loops. The method uses algorithmic combinatorics and
algebraic techniques. The approach is shown to be complete for some
special cases. By completeness we mean that it generates a set of
polynomial invariants from which, under additional assumptions, any
polynomial invariant can be derived. These techniques are implemented
in a new software package Aligator written in Mathematica and
successfully tried on many programs implementing interesting
algorithms working on numbers.",
paper = "Kova08.pdf",
keywords = "printed"
}\end{chunk}
\index{Oury, Nicolas}
\index{Swierstra, Wouter}
\begin{chunk}{ axiom.bib}
@inproceedings{Oury08,
author = "Oury, Nicolas and Swierstra, Wouter",
title = {{The Power of Pi}},
link = "\url{https://cs.ru. }",nl/~wouters/ Publications/ ThePowerOfPi. pdf
booktitle = "Int. Conf. on Functional Programming",
year = "2008",
abstract =
"This paper exhibits the power of programming with dependent types by
dint of embedding three domainspecific languages: Cryptol, a
language for cryptographic protocols; a small data description
language; and relational algebra. Each example demonstrates
particular design patterns inherent to dependentlytyped programming.
Documenting these techniques paves the way for further research in
domainspecific embedded type systems.",
paper = "Oury08.pdf",
keywords = "printed"
}\end{chunk}
\index{Graillat, Stef}
\index{Menissier Morain, Valerie}
\begin{chunk}{ axiom.bib}
@inproceedings{Grai07,
author = "Graillat, Stef and MenissierMorain, Valerie",
title = {{Errorfree Transformations in Real and Complex
Floating point Arithmetic}},
booktitle = "Int. Symp. on Nonlinear Theory and Applications",
year = "2007",
abstract =
"Errorfree transformation is a concept that makes it possible to
compute accurate results within a floating point arithmetic. Up to
now, it has only be studied for real floating point arithmetic. In
this short note, we recall the known errorfree transformations for
real arithmetic and we propose some new errorfree transformations for
complex floating point arithmetic. This will make it possible to
design some new accurate algorithms for summation, dot product and
polynomial evaluation with complex entries.",
paper = "Grai07.pdf"
}\end{chunk}
\index{Noblel, James}
\index{Black, Andrew P.}
\index{Bruce, Kim B.}
\index{Homer, Michael}
\index{Miller, Mark S.}
\begin{chunk}{ axiom.bib}
@inproceedings{Nobl16,
author = "Noble, James and Black, Andrew P. and Bruce, Kim B. and
Homer, Michael and Miller, Mark S.",
title = {{The Left Hand of Equals}},
booktitle = "Int. Symp. of New Ideas, New Paradigms, and Reflections
on Programming and Software",
publisher = "ACM",
pages = "224237",
year = "2016",
abstract =
"When is one object equal to another object? While object identity is
fundamental to objectoriented systems, object equality, although
tightly intertwined with identity, is harder to pin down. The
distinction between identity and equality is reflected in
objectoriented languages, almost all of which provide two variants of
'equality', while some provide many more. Programmers can usually
override at least one of these forms of equality, and can always
define their own methods to distinguish their own objects.This essay takes a reflexive journey through fifty years of identity
and equality in objectoriented languages, and ends somewhere we did
not expect: a 'lefthanded' equality relying on trust and grace.",
paper = "Nobl16.pdf",
keywords = "printed"
}\end{chunk}
\index{Avigad, Jeremy}
\begin{chunk}{ axiom.bib}
@article{Avig18a,
author = "Avigad, Jeremy"
title = {{The Mechanization of Mathematics}},
journal = "Notices of the AMS",
volume = "65",
number = "6",
year = "2018",
pages = "681690",
paper = "Avig18a.pdf",
keywords = "printed"
}\end{chunk}
\index{Leroy, Xavier}
\begin{chunk}{ axiom.bib}
@techreport{Lero90,
author = "Leroy, Xavier",
title = {{The ZINC experiment: An Economical Implementation of the
ML Language.}},
type = "technical report",
institution = "Institut National de Recherche en Informatique et en
Automatique" ,
number = "117",
year = "1990",
abstract =
"This report details the design and implementation of the ZINC
system. This is an implementation of the ML language, inended to
serve as a test field for various extensions of the language, and
for new implementation techniques as well. This system is strongly
oriented toward separate compilation and the production of small,
standalone programs; type safety is ensured by a Modula2like
module system. ZINC uses simple, portable techniques, such as
bytecode interpretation; a sophisticated execution model helps
counterbalance the interpretation overhead. Other highlights
include an efficient implementation of records with inclusion
(subtyping).",
paper = "Lero90.pdf",
keywords = "printed"
}\end{chunk}
\index{Cohn, Avra Jean}
\begin{chunk}{ axiom.bib}
@phdthesis{Cohn79,
author = "Cohn, Avra Jean",
title = {{Machine Assisted Proofs of Recursion Implementation}},
school = "University of Edinburgh",
year = "1979",
link = "\url{https://www.era. }",lib.ed. ac.uk/handle/ 1842/6643
abstract =
"Three studies in the machine assisted proof of recursion
implementation are described. The verification system used is
Edinburgh LCF (Logic for Computable Functions). Proofs are generated,
in LCF, in a goaloriented fashion by the application of strategies
reflecting informal proof plans. LCF is introduced in Chapter 1. We
present three case studies in which proof strategies are developed and
(except in the third) tested in LCF. Chapter 2 contains an account of
the machine generated proofs of three program transformations (from
recursive to iterative function schemata). Two of the examples are
taken from Manna and Waldinger. In each case, the recursion is
implemented by the introduction of a new data type, e.g., a stack or
counter. Some progress is made towards the development of a general
strategy for producing the equivalence proofs of recursive and
iterative function schemata by machine. Chapter 3 is concerned with
the machine generated proof of the correctness of a compiling
algorithm. The formulation, borrowed from Russell, includes a simple
imperative language with a while and conditional construct, and a low
level language of labelled statements, including jumps. We have, in
LCF, formalised his denotational descriptions of the two languages and
performed a proof of the preservation of the semantics under
compilation. In Chapter 4, we express and informally prove the
correctness of a compiling algorithm for a language containing
declarations and calls of recursive procedures. We present a low level
language whose semantics model a standard activation stack
implementation. Certain theoretical difficulties (connected with
recursively defined relations) are discussed, and a proposed proof in
LCF is outlined. The emphasis in this work is less on proving original
theorems, or even automatically finding proofs of known theorems, than
on (i) exhibiting and analysing the underlying structure of proofs,
and of machine proof attempts, and (ii) investigating the nature of
the interaction (between a user and a computer system) required to
generate proofs mechanically; that is, the transition from informal
proof plans to behaviours which cause formal proofs to be performed.",
paper = "Cohn79.pdf"
}\end{chunk}
\index{Russell, Bruce D.}
\begin{chunk}{ axiom.bib}
@article{Russ77,
author = "Russell, Bruce D.",
title = "Implementation Correctness Involving a Language with GOTO
statements" ,
journal = "SIAM Journal of Computing",
volume = "6",
number = "3",
year = "1977",
abstract =
"Two languages, one a simple structured programming language, the
other a simple goto language, are defined. A denotational semantics is
given for each language. An interpreter for the goto language is given
and is proved correct with respect to the denotational semantics. A
compiler from the structured to the goto language is defined and
proved to be a semantically invariant translation of programs. The
proofs are by computational induction.",
paper = "Russ77.pdf",
keywords = "printed"
}\end{chunk}
\index{Paulson, Lawrence C.}
\begin{chunk}{ axiom.bib}
@book{Paul87,
author = "Paulson, Lawrence C.",
title = {{Logic and Computation}},
publisher = "Press Synticate of Cambridge University",
year = "1987",
isbn = 0521346320"
}\end{chunk}
\index{Shoenfield, Joseph R.}
\begin{chunk}{ axiom.bib}
@book{Shoe67,
author = "Shoenfield, Joseph R.",
title = {{Mathematical Logic}},
publisher = "Association for Symbolic Logic",
year = "1967",
isbn = "1568811357"
}\end{chunk}
\index{Abramsky, S.}
\index{Gabbay, Dov M.}
\index{Maibaum, T.S.E}
\begin{chunk}{ axiom.bib}
@book{Abra92,
author = "Abramsky, S. and Gabbay, Dov M. and Maibaum, T.S.E",
title = {{Handbook of Logic in Computer Science (Volume 2)}},
publisher = "Oxford Science Publications",
year = "1992",
isbn = "0198537611"
}\end{chunk}
\index{Basu, Saugata}
\index{Pollack, Richard}
\index{Roy, MarieFrancoise}
\begin{chunk}{ axiom.bib}
@book{Basu10,
author = "Basu, Saugata and Pollack, Richard and Roy, MarieFrancoise",
title = {{Algorithms in Real Algebraic Geometry}},
publisher = "SpringerVerlag",
year = "2010",
isbn = "9783642069642"
}\end{chunk}
\index{Harrison, John}
\begin{chunk}{ axiom.bib}
@book{Harr09,
author = "Harrison, John",
title = {{Handbook of Practical Logic and Automated Reasoning}},
publisher = "Cambridge University Press",
year = "2009",
isbn = "9780521899574"
}\end{chunk}
\index{Barendregt, Henk}
\index{Dekkers, Wil}
\index{Statman, Richard}
\begin{chunk}{ axiom.bib}
@book{Bare13,
author = "Barendregt, Henk and Dekkers, Wil and Statman, Richard",
title = {{Lambda Calculus with Types}}
publisher = "Cambridge University Press",
year = "2013",
isbn = "9780521766142"
}\end{chunk}
\index{Manna, Zohar}
\index{Waldinger, Richard}
\begin{chunk}{ axiom.bib}
@book{Mann85,
author = "Manna, Zohar and Waldinger, Richard",
title = {{The Logical Basis for Computer Programming (Vol 1)}},
publisher = "AddisonWesley",
year = "1985",
isbn = "0201152602"
}\end{chunk}
\index{Pierce, Benjamin C.}
\begin{chunk}{ axiom.bib}
@book{Pier02,
author = "Pierce, Benjamin C.",
title = {{Types and Programming Languages}},
publisher = "MIT Press",
year = "2002",
isbn = "9780262162098"
}\end{chunk}
\index{Tarski, Alfred}
\begin{chunk}{ axiom.bib}
@book{Tars46,
author = "Tarski, Alfred",
title = {{Introduction to Logic}},
publisher = "Dover",
year = "1946",
isbn = "13978048628462 0"
}\end{chunk}
\index{Shankar, N.}
\begin{chunk}{ axiom.bib}
@book{Shan94,
author = "Shankar, N.",
title = {{Metamathematics, Machines, and Godel's Proof}},
publisher = "Cambridge University Press",
year = "1994",
isbn = "0521585333"
}\end{chunk}
\index{Beeson, Michael J.}
\begin{chunk}{ axiom.bib}
@book{Bees80,
author = "Beeson, Michael J.",
title = {{Foundations of Constructive Mathematics}}
publisher = "SpringerVerlag",
year = "1980",
isbn = "3540121730"
}\end{chunk}
\index{Shieber, Stuart M.}
\index{Schabes, Yves}
\index{Pereira, Fernando C.N.}
\begin{chunk}{ axiom.bib}
@article{Shie95,
author = "Shieber, Stuart M. and Schabes, Yves and Pereira, Fernando C.N.",
title = {{Principles and Implementation of Deductive Parsing}},
journal = "J. Logic Programming",
volume = "24",
number = "12",
pages = "336",
year = "1995",
abstract =
"We present a system for generating parsers based directly on the
metaphor of parsing as deduction. Parsing algorithms can be
represented directly as deduction systems, and a single deduction
engine can interpret such deduction systems so as to implement the
corresponding parser. The method generalizes easily to parsers for
augmented phrase structure formalisms, such as definiteclause
grammars and other logic grammar formalisms, and has been used for
rapid prototyping of parsing algorithms for a variety of formalisms
including variants of treeadjoining grammars, categorial grammars,
and lexicalized contextfree grammars.",
paper = "Shie95.pdf",
keywords = "printed"
}\end{chunk}
\index{Greve, David A.}
\index{Kaufmann, Matt}
\index{Manolios, Panagiotis}
\index{Moore, J Strother}
\index{Ray, Sandip}
\index{RuizReina, Jose Luis}
\index{Sumners, Rob}
\index{Vroon, Daron}
\index{Wilding, Matthew}
\begin{chunk}{ axiom.bib}
@article{Grev08,
author = "Greve, David A. and Kaufmann, Matt and Manolios, Panagiotis
and Moore, J Strother and Ray, Sandip and RuizReina, Jose Luis
and Sumners, Rob and Vroon, Daron and Wilding, Matthew",
title = {{Efficient Execution in an Automated Reasoning Environment}},
journal = "Journal of Functional Programming",
volume = "18",
number = "1",
pages = "1546",
year = "2008",
abstract =
"We describe a method that permits the user of a mechanized
mathematical logic to write elegant logical definitions while allowing
sound and efficient execution. In particular, the features supporting
this method allow the user to install, in a logically sound way,
alternative executable counterparts for logically defined
functions. These alternatives are often much more efficient than the
logically equivalent terms they replace. These features have been
implemented in the ACL2 theorem prover, and we discuss several
applications of the features in ACL2.",
paper = "Grev08.pdf",
keywords = "printed"}
\end{chunk}
\index{Appel, Andrew W.}
\index{MacQueen, David B.}
\begin{chunk}{ axiom.bib}
@inproceedings{Appe91,
author = "Appel, Andrew W. and MacQueen, David B.",
title = {{Standard ML of New Jersey}},
booktitle = "Int. Symp. on Prog. Lang. Implementations and Logic
Programming" ,
publisher = "SpringerVerlag",
pages = "113",
year = "1991",
abstract =
"The Standard ML of New Jersey compiler has been under development for
five years now. We have developed a robust and complete environment
for Standard ML that supports the implementation of large software
systems and generates efficient code. The compiler has also served as
a laboratory for developing novel implementation techniques for a
sophisticated type and module system, continuation based code
generation, efficient pattern matching, and concurrent programming
features.",
paper = "Appe91.pdf",
keywords = "printed"
}\end{chunk}
\index{Tofte, Mads}
\begin{chunk}{ axiom.bib}
@misc{Toft09,
author = "Tofte, Mads",
title = {{Tips for Computer Scientists on Standard ML (Revised)}},
link = "\url{http://www.itu. }",dk/people/ tofte/publ/ tips.pdf
year = "2009",
paper = "Toft09.pdf",
keywords = "printed"
}\end{chunk}
\index{Graham, Paul}
\begin{chunk}{ axiom.bib}
@book{Grah93,
author = "Graham, Paul",
title = {{On Lisp}},
publisher = "Prentice Hall",
year = "1993",
link = "\url{http://ep.yimg. }",com/ty/ cdn/paulgraham/ onlisp. pdf
comment = "code in papers/onlisp. lisp",
isbn = "0130305529",
abstract =
"On Lisp is a comprehensive study of advanced Lisp techniques, with
bottomup programming as the unifying theme. It gives the first
complete description of macros and macro applications. The book also
covers important subjects related to bottomup programming, including
functional programming, rapid prototyping, interactive development,
and embedded languages. The final chapter takes a deeper look at
objectoriented programming than previous Lisp books, showing the
stepbystep construction of a working model of the Common Lisp Object
System (CLOS).",
paper = "Grah93.pdf"
}\end{chunk}
\index{Loh, Andres}
\index{McBride, Conor}
\index{Swierstra, Wouter}
\begin{chunk}{ axiom.bib}
@misc{Lohx18,
author = "Loh, Andres and McBride, Conor and Swierstra, Wouter",
title = {{Simply Easy! An Implementation of a Dependently Typed
Lambda Calculus}},
link = "\url{http://strictlypositiv }",e.org/Easy. pdf
year = "2018",
abstract =
"We present an implementation in Haskell of a dependentlytyped
lambda calculus that can be used as the core of a programming
language. We show that a dependentlytyped lambda calculus is no
more difficult to implement than other typed lambda calculi. In fact,
our implementation is almost as easy as an implementation of the
simply typed lambda calculus, which we emphasize by discussing
the modifications necessary to go from one to the other. We explain
how to add data types and write simple programs in the core
language, and discuss the steps necessary to build a fullfledged
programming language on top of our simple core.",
paper = "Lohx18.pdf",
keywords = "printed"
}\end{chunk}
\index{Felty, Amy}
\index{Miller, Dale}
\begin{chunk}{ axiom.bib}
@techreport{Felt90,
author = "Felty, Amy and Miller, Dale",
title = {{Encoding a DependentType Lambda Calculus in a Logic
Programmin g Language}},
type = "technical report",
number = "MSCIS9018",
institution = "University of Pennsylvania",
year = "1990",
abstract =
"Various forms of typed $\lambda$calculi have been proposed as
specification languages for representing wide varieties of object
logics. The logical framework, LF, is an example of such a
dependenttype $\lambda$calculus. A small subset of intuitionistic
logic with quantification over simply typed $\lambda$calculus has
also been proposed as a framework for specifying general logics. The
logic of {\sl hereditary Harrop formulas} with quantification at all
nonpredicate types, denoted here as $hh^\omega$ , is such a
metalogic that has been implemented in both the Isabelle theorem
prover and the $\lambda$Prolog logic programming language. Both
frameworks provide for specifications of logics in which details
involved with free and bound variable occurrences, substitutions,
eigenvariables, and the scope of assumptions within object logics are
handled correctly and elegantly at the 'meta' level. In this paper, we
show how LF ca n be encoded into $hh^\omega$ in a direct and natural
way by mapping the typing judgments in LF in to propositions in the
logic of $hh^\omega$. This translation establishes a very strong
connection between these two languages: the order of quantification in
an LF signature is exactly the order of a set of $hh^\omega$ clauses,
and the proofs in one system correspond directly to proofs in the
other system. Relating these two languages makes it possible to
provide implementations of proof checkers and theorem provers for
logics specified in LF by using standard logic programming techniques
which can be used to implement $hh^\omega$.",
paper = "Felt90.pdf",
keywords = "printed"
}\end{chunk}
\index{Altenkirch, Thorsten}
\index{McBride, Conor}
\index{McKinna, James}
\begin{chunk}{ axiom.bib}
@misc{Alte05,
author = "Altenkirch, Thorsten and McBride, Conor",
title = {{Why Dependent Types Matter}},
link = "\url{http://www.cs. }",nott.ac. uk/~psztxa/ publ/ydtm. pdf
year = "2005",
abstract =
"We exhibit the rationale behind the design of Epigram, a dependently
typed programming language and interactive program development system,
using refinements of a well known program  merge sort  as a running
example. We discuss its relationship with other proposals to introduce
aspects of dependent types into functional programming languages and
sketch some topics for further work in this area.",
paper = "Alte05.pdf",
keywords = "printed"
}\end{chunk}
\index{Xi, Hongwei}
\index{Pfenning, Frank}
\begin{chunk}{ axiom.bib}
@inproceedings{Xixx99,
author = "Xi, Hongwei and Pfenning, Frank",
title = {{Dependent Types in Practical Programming}},
booktitle = "SIGPLANSIGACT Symp. on Principles of Programming
Languages" ,
year = "1990",
link = "\url{https://www.cs. }",cmu.edu/ ~fp/papers/ popl99. pdf
publisher = "ACM",
abstract =
"We present an approach to enriching the type system of ML with a
restricted form of dependent types, where type index objects are drawn
from a constraint domain C , leading to the DML( C ) language schema.
This allows specification and inference of significantly more precise
type information, facilitating program error detection and compiler
optimization. A major complication resulting from introducing
dependent types is that pure type inference for the enriched system is
no longer possible, but we show that typechecking a suciently
annotated program in DML( C ) can be reduced to constraint
satisfaction in the constraint domain C . We exhibit the
unobtrusiveness of our approach through practical examples and prove
that DML( C ) is conservative over ML. The main contribution of the
paper lies in our language design, including the formulation of
typechecking rules which makes the approach practical. To our
knowledge, no previous type system for a general purpose programming
language such as ML has combined dependent types with features including
datatype declarations, higherorder functions, general recursions,
letpolymorphism, mutable references, and exceptions. In addition,
we have finished a prototype implementation of DML( C ) for an integer
constraint domain C , where constraints are linear inequalities (Xi
and Pfenning 1998).",
paper = "Xixx99.pdf",
keywords = "printed"
}\end{chunk}
\index{Altenkirch, Thorsten}
\begin{chunk}{ axiom.bib}
@misc{Alte04,
author = "Altenkirch, Thorsten",
title = {{$\lambda$calculus and types}},
comment = "Lecture Notes; APPSEM Spring School 2004",
link = "\url{http://www.cs. }",nott.ac. uk/~psztxa/ publ/mgs04. pdf
year = "2004"
paper = "Alte04.pdf",
keywords = "printed",
}\end{chunk}
\index{Loh, Andres}
\index{McBride, Conor}
\index{Swierstra, Wouter}
\begin{chunk}{ axiom.bib}
@article{Lohx01,
author = "Loh, Andres and McBride, Conor and Swierstra, Wouter",
title = {{A Tutorial Implementation of a Dependently Typed Lambda
Calculus} },
journal = "Fundamenta Informaticae",
volume = "XXI",
year = "2001",
pages = "10011031",
abstract =
"We present the type rules for a dependently typed core calculus
together with a straightforward implementation in Haskell. We
explicitly highlight the changes necessary to shift from a
simplytyped lambda calculus to the dependently typed lambda
calculus. We also describe how to extend our core language with data
types and write several small example programs. The article is
accompanied by an executable interpreter and example code that allows
immediate experimentation with the system we describe.",
paper = "Lohx01.pdf",
keywords = "printed"
}\end{chunk}
\index{Roorda, JanWillem}
\begin{chunk}{ axiom.bib}
@phdthesis{Roor00,
author = "Roorda, JanWillem",
title = {{Pure Type Systems for Functional Programming}},
year = "2000",
institution = "University of Utrecht",
abstract =
"We present a functional programming language based on Pure Type
Systems (PTSs). We show how we can define such a language by
extending the PTS framework with algebraic data types, case
expressions and definitions. To be able to experiment with our
language we present an implementation of a type checker and an
interpreter for our language. PTSs are well suited as a basis for a
functional programming language because they are at the top of a
hierarchy of increasingly stronger type systems. The concepts of
`existential types', `rankn polymorphism' and `dependent types' arise
naturally in functional programming languages based on the systems in
this hierarchy. There is no need for adhoc extensions to incorporate
these features. The type system of our language is more powerful than
the HindleyMilner system. We illustrate this fact by giving a number
of meaningful programs that cannot be typed in Haskell but are typable
in our language. A `real world' example of such a program is the
mapping of a specialisation of a Generic Haskell function to a Haskell
function. Unlike the description of the Henk language by Simon Peyton
Jones and Erik Meijer we give a complete formal definition of the type
system and the operational semantics of our language. Another
difference between Henk and our language is that our language is
defined for a large class of Pure Type Systems instead of only for the
systems of the $\lambda$cube.",
paper = "Roor00.pdf",
keywords = "printed"
}\end{chunk}
\index{Jones, Simon Peyton}
\index{Meijer, Erik}
\begin{chunk}{ axiom.bib}
@misc{Jone97,
author = "Jones, Simon Peyton and Meijer, Erik",
title = {{Henk: A Typed Intermediate Language}},
year = "1997",
link =
"\url{https://www.microsoft. }",com/en us/research/ wpcontent/ uploads/ 1997/01/ henk.pdf
abstract =
"There is a growing interest in the use of richlytyped
intermediate languages in sophisticated compilers for
higherorder, typed source languages. These intermediate languages
are typically stratified, involving terms, types, and kinds. As
the sophistication of the type system increases, there three
levels begin to look more and more similar, so an attraictive
approach is to use a single syntax, and a single data type in the
compiler, to represent all three.The theory of socalled {\sl pure type systems} amkes precisely
such an identification. This paper describes Henk, a new typed
intermediate langugage based closely on a particuarl pure type
system, {\sl the lambda cube}. On the way we give a tutorial
introduction to the lambda cube.",
paper = "Jone97.pdf",
keywords = "printed"
}\end{chunk}
\index{Morrisett, Greg}
\begin{chunk}{ axiom.bib}
@phdthesis{Morr95,
author = "Morrisett, Greg",
title = {{Compiling with Types}},
school = "Carnegie Mellon University",
year = "1995",
comment = "CMUCS95226",
link = "\url{https://www.cs. }",cmu.edu/ ~rwh/theses/ morrisett. pdf
abstract =
"Compilers for monomorphic languages, suc h as C and Pascal, take
advantage of types to determine data representations, alignment,
calling conventions, and register selection. However, these languages
lack important features including polymorphism, abstract datatypes,
and garbage collection. In contrast, modern programming languages
such as Standard ML (SML), provide all of these features, but existing
implementations fail to take full advantage of types. The result is
that performance of SML code is quite bad when compared to C.In this thesis, I provide a general framework, called
{\sl typedirected compilation}, that allows compiler writeres to
take advantage of types at all stages in compilation. In the
framework, types are used not only to determine efficient
representations and calling conventions, but also to prove the
correctness of the compiler. A key property of typedirected
compilation is that all but the lowest levels of the compiler use
{\sl typed intermediate languages}. An advantage of this approach
is that it provides a means for automatically checking the
integrity of the resulting code.An mportant contribution of this work is the development of a new,
staticallytyped intermediate language, called $\lambda^{ML}_i$.
This language supports {\sl dynamic type dispatch}, providing a
means to select operations based on types at run time. I show how
to use dynamic type dispatch to support polymorphism, adhoc
operators, and garbage collection without having to box or tag
values. This allows compilers for SML to take advantage of
techniques used in C compilers, without sacrificing language
features or separate compilation.TO demonstrate the applicability of my approach, I, along with
others, have constructed a new compiler for SML called TIL that
eliminates most restrictions on the representations of values. The
code produced by TIL is roughly twice as fast as code produced by
the SML/NJ compiler. This is due to at least partially to the use
of natural representations, but primarily to the conventional
optimizer which manipulates typed, $\lambda^{ML}_i$ code. TIL
demonstrates that combining typedirected compilation with dynamic
type dispatch yields a superior architecture for compilers of
modern languages.",
paper = "Morr95.pdf"
}\end{chunk}
\index{Leroy, Xavier}
\begin{chunk}{ axiom.bib}
@article{Lero98,
author = "Leroy, Xavier",
title = {{An Overview of Types in Compilation}},
journal = "LNCS",
volume = "1473",
year = "1998",
publisher = "SpringerVerlang",
pages = "18",
paper = "Lero98.pdf",
keywords = "printed"
}\end{chunk}
\index{Lu, Eric}
\begin{chunk}{ axiom.bib}
@misc{Luxx16,
author = "Lu, Eric",
title = {{Barendregt's Cube and Programming with Dependent Types}},
link = "\url{https://www.seas. }",harvard. edu/courses/ cs252/2016fa/ 15.pdf
paper = "Luxx16.pdf",
keywords = "printed"
}\end{chunk}
\index{Guallart, Nino}
\begin{chunk}{ axiom.bib}
@misc{Gual14,
author = "Guallart, Nino",
title = {{An Overview of Type Theories}},
link = "\url{https://arxiv. }",org/pdf/ 1411.1029. pdf
year = "2014",
abstract =
"Pure type systems arise as a generalisation of simply typed lambda
calculus. The contemporary development of mathematics has renewed
the interest in type theories, as they are not just the object of
mere historical research, but have an active role in the development
of computational science and core mathematics. It is worth exploring
some of them in depth, particularly predicative MartinLöf’s
intuitionistic type theory and impredicative Coquand’s calculus of
constructions. The logical and philosophical differences and
similarities between them will be studied, showing the relationship
between these type theories and other fields of logic.",
paper = "Gual14.pdf",
keywords = "printed"
}\end{chunk}
\index{Benini, Marco}
\begin{chunk}{ axiom.bib}
@misc{Beni95,
author = "Benini, Marco",
title = {{Barendregt's $\lambda$Cube in Isabelle}},
link = "\url{}",
year = "1995",
abstract =
"We present an implementation of Barendregt’s $\lambda$Cube in the
Isabelle proof system. Isabelle provides many facilities for
developing a useful specification and proving environment from the
basic formulation of formal systems. We used those facilities to
provide an environment where the user can describe problems and derive
proofs interactively.",
paper = "Beni95.pdf",
keywords = "printed"
}\end{chunk}
\index{Hellman, Martin E.}
\begin{chunk}{ axiom.bib}
@article{Hell17,
author = "Hellman, Martin E.",
title = {{Cybersecurity, Nuclear Security, Alan Turing, and
Illogical Logic}},
journal = "J. ACM",
volume = "60",
number = "12",
pages = "5259",
year = "2017",
link = "\url{https://cacm.acm. }"org/magazines/ 2017/12/ 223042 cybersecurity nuclear security alanturing andillogical logic/fulltext
}\end{chunk}
\index{Winston, Patrick Henry}
\begin{chunk}{ axiom.bib}
@inproceedings{Wins12,
author = "Winston, Patrick Henry",
title = {{The Nex 50 Years: A Personal View}},
booktitle = "Biologially Inspired Cognitive Architectures 1",
year = "2012",
pages = "9299",
publisher = "Elsevier B.V"
abstract =
"I review history, starting with Turing’s seminal paper, reaching
back ultimately to when our species started to outperform other
primates, searching for the questions that will help us develop a
computational account of human intelligence. I answer that the
right questions are: What’s different between us and the other
primates and what’s the same. I answer the {\sl what’s different}
question by saying that we became symbolic in a way that enabled
story understanding, directed perception, and easy communication,
and other species did not. I argue against Turing’s
reasoningcentered suggestions, offering that reasoning is just a
special case of story understanding. I answer the {\sl what’s the
same} question by noting that our brains are largely engineered in
the same exotic way, with information flowing in all directions at
once. By way of example, I illustrate how these answers can
influence a research program, describing the Genesis system, a
system that works with short summaries of stories, provided in
English, together with lowlevel {\sl commonsense rules} and
higherlevel {\sl concept patterns}, likewise expressed in
English. Genesis answers questions, notes abstract concepts such
as {\sl revenge}, tells stories in a listeneraware way, and fills
in story gaps using precedents. I conclude by suggesting,
optimistically, that a genuine computational theory of human
intelligence will emerge in the next 50 years if we stick to the
right, biologically inspired questions, and work toward
biologically informed models.",
paper = "Wins12.pdf"
}\end{chunk}
\index{Brooks, Rodney A.}
\begin{chunk}{ axiom.bib}
@article{Broo87,
author = "Brooks, Rodney A.",
title = {{Intelligence Without Representation}},
journal = "Artificial Intelligence",
volume = "47",
year = "1991",
pages = "139159",
abstract =
"Artificial intelligence research has foundered on the issue of
representation. When intelligence is approached in an incremental
manner, with strict reliance on interfacing to the real world through
perception and action, reliance on representation disappears. In this
paper we outline our approach to incrementally building complete
intelligent Creatures. The fundamental decomposition of the
intelligent system is not into independent information processing
units which must interface with each other via representations.
Instead, the intelligent system is decomposed into independent and
parallel activity producers which all interface directly to the world
through perception and action, rather than interface to each other
particularly much. The notions of central and peripheral systems
evaporateeverything is both central and peripheral. Based on these
principles we have built a very successful series of mobile robots
which operate without supervision as Creatures in standard office
environments.",
paper = "Broo87.pdf"
}\end{chunk}
\index{Roy, Peter Van}
\index{Haridi, Seif}
\begin{chunk}{ axiom.bib}
@book{Royx03,
author = "Roy, Peter Van and Haridi, Seif",
title = {{Concepts, Techniques, and Models of Computer Programming}},
year = "2003",
link =
"\url{http://citeseerx. }",ist.psu. edu/viewdoc/ download? doi=10. 1.1.102. 7366&rep= rep1&type= pdf
publisher = "MIT",
isbn = "9780262220699",
paper = "Royx03.pdf"
}\end{chunk}
\index{Boyer, Robert S.}
\index{Moore, J Strother}
\begin{chunk}{ axiom.bib}
@article{Boye84,
author = "Boyer, Robert S. and Moore, J Strother",
title = {{ProofChecking, TheoremProving, and Program Verification}},
journal = "Contemporary Mathematics",
volume = "29",
year = "1984",
abstract =
"This article consists or three parts: a tutorial introduction to a
computer program that proves theorems by induction; a brief
description or recent applications or that theoremprover; and a
discussion or several nontechnical aspects of the problem or building
automatic theoremprovers. The theoremprover described has proved
theorems such as the uniqueness of prime factorizations, Fermat's
theorem, and the recursive unsolvability or the halting problem.The article is addressed to those who know nothing about automatic
theoremproving but would like a glimpse or one such system. This
article definitely does not provide a balanced view or all automatic
theoremproving, the literature of which is already rather large and
technica1. Nor do we describe the details or our theoremproving
system, but they can be round in the books, articles, and technical
reports that we reference.In our opinion, progress in automatic theoremproving is largely a
function or the mathematical ability or those attempting to build such
systems. We encourage good mathematicians to work in the field.",
paper = "Boye84.pdf",
keywords = "printed"
}\end{chunk}
\index{Lamport, Leslie}
\begin{chunk}{ axiom.bib}
@article{Lamp78
author = "Lamport, Leslie",
title = {{The Specification and Proof of Correctness of Interactive
Programs} },
journal = "LNCS",
volume = "75",
year = "1978",
abstract =
"method production assertional rules specified, is proved is modified
correctly to accept and interactive is described, method that a
program A program of specifying and to permit typed its implementation
correct. by and the FloydHoare implements format programs one to
prove its specification. input is formally with a TECO program.",
paper = "Lamp78.pdf",
keywords = "printed"
}\end{chunk}
\index{Anderson, E.R.}
\index{Belz, F.C.}
\index{Blum, E.K.}
\begin{chunk}{ axiom.bib}
@article{Ande78,
author = "Anderson, E.R. and Belz, F.C. and Blum, E.K.",
title = {{Extending an Implementation Language to a Specification Language}},
journal = "LNCS",
volume = "75",
year = "1978",
paper = "Ande78.pdf",
keywords = "printed"
}\end{chunk}
\index{
TobinHochstadt , Sam}
\index{Felleisen, Matthias}
\begin{chunk}{ axiom.bib}
@misc{Tobi11,
author = "TobinHochstadt, Sam and Felleisen, Matthias",
title = {{The Design and Implementation of Typed Scheme: From
Scripts to Programs}},
link = "\url{https://arxiv. }",org/pdf/ 1106.2575. pdf
year = "2011",
abstract =
"When scripts in untyped languages grow into large programs,
maintaining them becomes difficult. A lack of explicit type
annotations in typical scripting languages forces programmers to must
(re)discover critical pieces of design information every time they
wish to change a program. This analysis step both slows down the
maintenance process and may even introduce mistakes due to the
violation of undiscovered invariants.This paper presents Typed Scheme, an explicitly typed extension of PLT
Scheme, an untyped scripting language. Its type system is based on
the novel notion of occurrence typing, which we formalize and
mechanically prove sound. The implementation of Typed Scheme
additionally borrows elements from a range of approaches, including
recursive types, true unions and subtyping, plus polymorphism combined
with a modicum of local inference.The formulation of occurrence typing naturally leads to a simple and
expressive version of predicates to describe refinement types. A
Typed Scheme program can use these refinement types to keep track of
arbitrary classes of values via the type system. Further, we show how
the Typed Scheme type system, in conjunction with simple recursive
types, is able to encode refinements of existing datatypes, thus
expressing both proposed variations of refinement types.",
paper = "Tobi11.pdf",
keywords = "printed"
}\end{chunk}
\index{McCarthy, John}
\index{Painter, James}
\begin{chunk}{ axiom.bib}
@inproceedings{Mcca67,
author = "McCarthy, John and Painter, James",
title = {{Correctness of a Compiler for Arithmetic Expressions}},
booktitle = "Proc. Symp. in Applied Mathematics",
publisher = "American Mathematical Society",
year = "1967",
paper = "Mcca67.pdf",
keywords = "printed"
}\end{chunk}
\index{Vuillemin, Jean}
\begin{chunk}{ axiom.bib}
@phdthesis{Vuil73,
author = "Vuillemin, Jean",
title = {{Proof Techniques for Recursive Programs}},
school = "Stanford University",
year = "1973",
abstract =
"The concept of least fixedpoint of a continuous function can be
considered as the unifying thread of this dissertation.The connections between fixedpoints and recursive programs are
detailed in chapter 2, providing some insights on practical
implementations of recursion. There are two usual characterizations
of the least fixedpoint of a continuous function. To the first
characterization, due to Knaster and Tarski, corresponds a class
of proof techniques for programs, as described in Chapter 3. The
other characterization of least fixed points, better known as
Kleene's first recursion theorem, is discussed in Chapter 4. It
has the advantage of being effective and it leads to a wider class
of proof techniques.",
paper = "Vuil73.pdf"
}\end{chunk}
\begin{
chunk}{ axiom.bib}
@misc{Byte79,
author = "Byte Publications",
title = {{LISP}},
link = "\url{https://ia802603. }",us.archive. org/30/ items/byte magazine 197908/ 1979_08_ BYTE_04 08_LISP. pdf
publisher = "McGrawHill",
year = "1979",
paper = "Byte79.pdf"
}\end{chunk}
\index{Manna, Zohar}
\index{Vuillemin, Jean}
\begin{chunk}{ axiom.bib}
@article{Mann72,
author = "Manna, Zohar and Vuillemin, Jean",
title = {{Fixpoint Approach to the Theory of Computation}},
journal = "Communications of the ACM",
volume = "15",
number = "7",
year = "1972",
pages = "828836",
abstract =
"Following the fixpoint theory of Scott, the semantics of computer
programs are defined in terms of the least fixpoints of recursive
programs. This allows not only the justification of all existing
verification techniques, but also their extension to the handling, in
a uniform manner of various properties of computer programs, including
correctness, termination, and equivalence.",
paper = "Mann72.pdf",
keywords = "printed"
}\end{chunk}
\index{Paulson, Lawrence C.}
\begin{chunk}{ axiom.bib}
@article{Paul83,
author = "Paulson, Lawrence C.",
title = {{A HigherOrder Implementation of Rewriting}},
journal = "Science of Computer Programming",
volume = "3",
pages = "119149",
year = "1983",
abstract =
"Many automatic theoremprovers rely on rewriting. Using theorems as
rewrite rules helps to simplify the subgoals that arise during a
proof. LCF is an interactive theoremprover intended For reasoning
about computation. Its implementation of rewriting is presented in
detail. LCF provides a Family of rewriting Functions, and operators to
combine them. A succession of Functions is described, From pattern
matching primitives to the rewriting tool that performs most
inferences in LCF proofs. The design is highly modular. Each function
performs a basic, specific task, such as recognizing a certain form of
tautology. Each operator implements one method of building a rewriting
Function From simpler ones. These pieces can be put together in
numerous ways, yielding a variety of rewriting strategies. The
approach involves programming with higherorder Functions. Rewriting
Functions are data values, produced by computation on other rewriting
Functions. The code is in daily use at Cambridge, demonstrating the
practical use of Functional programming.",
paper = "Paul83.pdf",
keywords = "printed"
}\end{chunk}
\index{Avigad, Jeremy}
\index{Holzl, Johannes}
\index{Serafin, Luke}
@misc{Avig17c,
author = "Avigad, Jeremy and Holzl, Johannes and Serafin, Luke",
title = {{A Formally Verified Proof of the Central Limit Theorem}},
link = "\url{}",
year = "2017",
abstract =
"We describe a proof of the Central Limit Theorem that has been
formally verified in the Isabelle proof assistant. Our formalization
builds upon and extends Isabelle’s libraries for analysis and
measuretheoretic probability. The proof of the theorem uses
characteristic functions , which are a kind of Fourier transform, to
demonstrate that, under suitable hypotheses, sums of random
variables converge weakly to the st andard normal distribution. We
also discuss the libraries and infrastructure that supported the
formalization, and reflect on some of the lessons we have learned
from the effort.",
paper = "Avig17c.pdf",
keywords = "printed"
}\end{chunk}
\index{Feferman, Solomon}
\begin{chunk}{ axiom.bib}
@misc{Fefe95,
author = "Feferman, Solomon",
title = {{Definedness}},
year = "1995",
link = "\url{https://math.stanford. }",edu/~feferman/ papers/ definedness. pdf
abstract =
"Questions of definedness are ubiquitous in mathematics. Informally,
these involve reasoning about expressions which may or may not have a
value. This paper surveys work on logics in which such reasoning can
be carried out directly, especially in computational contexts. It
begins with a general logic of 'partial terms', continues with partial
combinatory and lambda calculi, and concludes with an expressively
rich theory of partial functions and polymorphic types, where
termination of functional programs can be established in a natural way.",
paper = "Fefe95.pdf",
keywords = "printed"
}\end{chumk}
 2871. By daly on 20180607

books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Kohlhase, Michael}
\index{De Feo, Luca}
\index{Muller, Dennis}
\index{Pfeiffer, Markus}
\index{Rabe, Florian}
\index{Thiery, Nicolas M.}
\index{Vasilyev, Victor}
\index{Wesing, Tom}
\begin{chunk}{ axiom.bib}
@inproceedings{Kohl17,
author = "Kohlhase, Michael and De Feo, Luca and Muller, Dennis and
Pfeiffer, Markus and Rabe, Florian and Thiery, Nicolas M.
and Vasilyev, Victor and Wesing, Tom",
title = {{KnowledgeBased Interoperability for Mathematical Software
Systems} },
booktitle = "7th Int. Conf. on Mathematical Aspects of Computer and
Information Sciences",
publisher = "Springer",
year = "2017",
pages = "195210",
isbn = "9783319724539",
abstract =
"There is a large ecosystem of mathematical software systems.
Individually, these are optimized for particular domains and
functionalities, and together they cover many needs of practical and
theoretical mathematics. However, each system specializes on one area,
and it remains very difficult to solve problems that need to involve
multiple systems. Some integrations exist, but the are adhoc and have
scalability and maintainability issues. In particular, there is not
yet an interoperability layer that combines the various systems into a
virtual research environment (VRE) for mathematics.The OpenDreamKit project aims at building a toolkit for such VREs. It
suggests using a central systemagnostic formalization of mathematics
(Mathinthe Middle, MitM) as the needed interoperability layer. In
this paper, we conduct the first major case study that instantiates
the MitM paradigm for a concrete domain as well as a concrete set of
systems. Specifically, we integrate GAP, Sage, and Singular to perform
computation in group and ring theory.Our work involves massive practical efforts, including a novel
formalization of computational group theory, improvements to the
involved software systems, and a novel mediating system that sits at
the center of a starshaped integration layout between mathematical
software systems.",
paper = "Kohl17.pdf",
keywords = "printed"
}\end{chunk}
\index{Dehaye, PaulOlivier}
\index{Iancu, Mihnea}
\index{Kohlhase, Michael}
\index{Konovalov, Alexander}
\index{Lelievre, Samuel}
\index{Muller, Dennis}
\index{Pfeiffer, Markus}
\index{Rabe, Florian}
\index{Thiery, Nicolas M.}
\index{Wiesling, Tom}
\begin{chunk}{ axiom.bib}
@inproceedings{Deha16,
author = "Dehaye, PaulOlivier and Iancu, Mihnea and Kohlhase, Michael
and Konovalov, Alexander and Lelievre, Samuel and
Muller, Dennis and Pfeiffer, Markus and Rabe, Florian and
Thiery, Nicolas M. and Wiesling, Tom",
title = {{Interoperability in the OpenDreamKit project: The
Math inthe Middle Approach}},
booktitle = "Intelligent Computer Mathematics",
pages = "117131",
year = "2016",
isbn = "9783319425467",
publisher = "Springer",
abstract =
"OpenDreamKit  'Open Digital Research Environment Toolkit for the
Advancement of Mathematics'  is an H2020 EU Research Infrastructure
project that aims at supporting, over the period 20152019, the
ecosystem of opensource mathematical software systems. OpenDreamKit
will deliver a flexible toolkit enabling research groups to set up
Virtual Research Environments, customised to meet the varied needs of
research projects in pure mathematics and applications.An important step in the OpenDreamKit endeavor is to foster the
interoperability between a variety of systems, ranging from
computer algebra systems over mathematical databases to
frontends. This is the mission of the integration work
package. We report on experiments and future plans with the
Mathinthe Middle approach. This architecture consists of a
central mathematical ontology that documents the domain and fixes a
joint vocabulary, or even a language, going beyond existing
systems such as OpenMath, combined with specifications of the
functionalities of the various systems. Interaction between
systems can then be enriched by pivoting around this architecture.",
paper = "Deha16.pdf",
keywords = "printed, axiomref"
}\end{chunk}
\index{de Bruijn, N.G.}
\begin{chunk}{ axiom.bib}
@techreport{Brui68a,
author = "de Bruijn, N.G.",
title = {{AUTOMATH, A Language for Mathematics}},
year = "1968",
type = "technical report",
number = "68WSK05",
institution = "Technische Hogeschool Eindhoven",
paper = "Brui68a.pdf"
}\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@article{Farm07a,
author = "Farmer, William M.",
title = {{Chiron: A MultiParadigm Logic}},
journal = "Studies in Logic, Grammar and Rhetoric",
volume = "10",
number = "23",
year = "2007",
abstract =
"Chiron is a derivative of vonNeumannBernays G̈odel ( NBG ) set
theory that is intended to be a practical, generalpurpose logic for
mechanizing mathematics. It supports several reasoning paradigms by
integrating NBG set theory with elements of type theory, a scheme for
handling undefinedness, and a facility for reasoning about the syntax
of expressions. This paper gives a quick, informal presentation of
the syntax and semantics of Chiron and then discusses some of the
benefits Chiron provides as a multiparadigm logic.",
paper = "Farm07a.pdf",
keywords = "axiomref, printed"
}\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@techreport{Farm13,
author = "Farmer, William M.",
title = {{Chiron: A Set Theory with Types, Undefinedness, Quotation,
and Evaluation}},
type = "technical report",
institution = "McMaster University",
number = "SQRL Report No. 38",
year = "2013",
link = "\url{https://arxiv. }",org/pdf/ 1305.6206. pdf
abstract =
"Chiron is a derivative of vonNeumannBernays Godel (NBG) set
theory that is intended to be a practical, generalpurpose logic for
mechanizing mathematics. Unlike traditional set theories such as
ZermeloFraenkel (ZF) and NBG, Chiron is equipped with a type system,
lambda notation, and definite and indefinite description. The type
system includes a universal type, dependent types, dependent function
types, subtypes, and possibly empty types. Unlike traditional logics
such as firstorder logic and simple type theory, Chiron admits
undefined terms that result, for example, from a function applied to
an argument outside its domain or from an improper definite or
indefinite description. The most noteworthy part of Chiron is its
facility for reasoning about the syntax of expressions. Quotation is
used to refer to a set called a construction that represents the
syntactic structure of an expression, and evaluation is used to refer
to the value of the expression that a construction represents. Using
quotation and evaluation, syntactic side conditions, schemas,
syntactic transformations used in deduction and computation rules, and
other such things can be directly expressed in Chiron. This paper
presents the syntax and semantics of Chiron, some definitions and
simple examples illustrating its use, a proof system for Chiron, and a
notion of an interpretation of one theory of Chiron in another.",
paper = "Farm13.pdf"
}\end{chunk}
\index{Kripke, Saul}
\begin{chunk}{ axiom.bib}
@article{Krip75,
author = "Kripke, Saul",
title = {{Outline of a Theory of Truth}},
journal = "Journal of Philosophy",
volume = "72",
number = "19",
year = "1975",
pages = "690716",
paper = "Krip75.pdf",
keywords = "printed"
}\end{chunk}
\index{Kleene, Stephen Cole}
\begin{chunk}{ axiom.bib}
@book{Klee52,
author = "Kleene, Stephen Cole",
title = {{Introduction to MetaMathematics}},
year = "1952",
publisher = "Ishi Press International",
isbn = "9780923891572",
paper = "Klee52.pdf"
}\end{chunk}
\index{Smith, Peter}
\begin{chunk}{ axiom.bib}
@misc{Smit15,
author = "Smith, Peter",
title = {{Some Big Books on Mathematical Logic}},
year = "2015",
link = "\url{}",
paper = "Smit15.pdf",
keywords = "printed"
}\end{chunk}
\index{Gonthier, Georges}
\begin{chunk}{ axiom.bib}
@article{Gont09a,
author = "Gonthier, Georges",
title = {{Software Engineering for Mathematics}},
journal = "LNCS",
volume = "5625",
year = "2009",
pages = "2727",
abstract =
"Despite its mathematical origins, progress in computer assisted
reasoning has mostly been driven by applications in computer science,
like hardware or protocol security verification. Paradoxically, it has
yet to gain widespread acceptance in its original domain of
application, mathematics; this is commonly attributed to a 'lack of
libraries': attempts to formalize advanced mathematics get bogged down
into the formalization of an unwieldly large set of basic resuts.This problem is actually a symptom of a deeper issue: the main
function of computer proof systems, checking proofs down to their
finest details, is at odds with mathematical practice, which ignores
or defers details in order to apply and combine abstractions in
creative and elegant ways. Mathematical texts commonly leave logically
important parts of proofs as 'exercises to the reader', and are rife
with 'abuses of notation that make mathematics tractable' (according
to Bourbaki). This (essential) flexibility cannot be readily
accomodated by the narrow concept of 'proof library' used by most
proof assistants and based on 19th century firstorder logic: a
collection of constants, definitions, and lemmas.This mismatch is familiar to software engineers, who have been
struggling for the past 50 years to reconcile the flexibility needed
to produce sensible user requirements with the precision needed to
implement them correctly with computer code. Over the last 20 years
object and components have replaced traditional data and procedure
libraries, partly bridging this gap and making it possible to build
significantly larger computer systems.These techniques can be implemented in compuer proof systems by
exploiting advances in mathematical logic. Higherorder logics allow
the direct manipulation of functions; this can be used to assign
behaviour, such as simplification rules, to symbols, similarly to
objects. Advanced type systems can assign a secondary, contextual
meaning to expressions, using mechanisms such as type classes,
similarly to the metadata in software components. The two can be combined
to perform reflection, where an entire statement gets quoted as
metadata and then proved algorithmically by some decision procedure.We propose to use a more modest, smallscale form of reflection, to
implement mathematical components. We use the typederived metadata to
indicate how symbols, definitions and lemmas should be used in other
theories, and functions to implement this usage — roughly, formalizing
some of the exercize section of a textbook. We have applied
successfully this more engineered approch to computer proofs in our
past work on the Four Color Theorem, the CayleyHamilton Theorem, and
our ongoing longterm effort on the Odd Order Theorem, which is the
starting point of the proof of the Classification of Finite Simple
Groups (the famous 'monster theorem' whose proof spans 10,000 pages in
400 articles).",
paper = "Gont09a.pdf",
keywords = "printed"
}\end{chunk}
\index{Carette, Jacques}
\begin{chunk}{ axiom.bib}
@article{Care10,
author = "Carette, Jacques",
title = {{Mechanized Mathematics}},
journal = "LNCS",
volume = "6167",
year = "2010",
pages = "157157",
abstract =
"In the 50 years since McCarthy’s 'Recursive Functions of Symbolic
Expressions and Their Computation by Machine', what have we
learned about the realization of Leibniz’s dream of just being
able to utter 'Calculemus!' (Let us calculate!) when faced with a
mathematical dilemma?In this talk, I will first present what I see as the most
important lessons from the past which need to be heeded by modern
designers. From the present, I will look at the context in which
computers are used, and derive further requirements. In
particular, now that computers are no longer the exclusive
playground for highly educated scientists, usability is now more
important than ever, and justifiably so.I will also examine what I see as some principal failings of
current systems, primarily to understand some major mistakes to
avoid. These failings will be analyzed to extract what seems to be
the root mistake, and I will present my favourite solutions.Furthermore, various technologies have matured since the creation
of many of our systems, and whenever appropriate, these should be
used. For example, our understanding of the structure of
mathematics has significantly increased, yet this is barely
reflected in our libraries. The extreme focus on efficiency by the
computer algebra community, and correctness by the (interactive)
theorem proving community should no longer be considered viable
long term strategies. But how does one effectively bridge that
gap?I personally find that a number of (programming) languagebased
solutions are particularly effective, and I will emphasize
these. Solutions to some of these problems will be illustrated
with code from a prototype of MathScheme 2.0, the system I am
developing with Bill Farmer and our research group.",
paper = "Care10.pdf",
keywords = "printed"
}\end{chunk}
\index{Zeilberger, Doron}
\begin{chunk}{ axiom.bib}
@article{Zeil10,
author = "Zeilberger, Doron",
title = {{Against Rigor}},
journal = "LNCS",
volume = "6167",
year = "2010",
pages = "262262",
abstract =
"The ancient Greeks gave (western) civilization quite a few
gifts, but we should beware of Greeks bearing gifts. The gifts of theatre
and democracy were definitely good ones, and perhaps even the gift of
philosophy, but the 'gift' of the socalled 'axiomatic method' and the
notion of 'rigorous' proof did much more harm than good. If we want
to maximize Mathematical Knowledge, and its Management, we have to
return to Euclid this dubious gift, and giveup our fanatical insistence
on perfect rigor. Of course, we should not go to the other extreme, of
demanding that everything should be nonrigorous. We should encourage
diversity of proofstyles and rigor levels, and remember that nothing is
absolutely sure in this world, and there does not exist an absolutely
rigorous proof, nor absolute certainty, and 'truth' has many shades and
levels.",
paper = "Zeil10.pdf",
keywords = "printed"
}\end{chunk}
\index{Pfenning, Frank}
\begin{chunk}{ axiom.bib}
@phdthesis{Pfen87,
author = "Pfenning, Frank",
title = {{Proof Transformations in HigherOrder Logic}},
year = "1987",
school = "Carnegie Mellon University",
link = "\url{http://wwwcgi. }",cs.cmu. edu/~fp/ papers/ thesis87. pdf
abstract =
"We investigate the problem of translating between different styles of
proof systems in higherorder logic: analytic proofs which are well
suited for automated theorem proving, and nonanalytic deductions
which are well suited for the mathematician. Analytic proofs are
represented as expansion proofs, $H$ , a form of the sequent calculus we
define, nonanalytic proofs are represented by natural deductions. A
nondeterministic translation algorithm between expansion proofs and
$H$deductions is presented and its correctness is proven. We also
present an algorithm for translation in the other direction and prove
its correctness. A cutelimination algorithm for expansion proofs is
given and its partial correctness is proven. Strong termination of
this algorithm remains a conjecture for the full higherorder
system, but is proven for the firstorder fragment. We extend the
translations to a nonanalytic proof system which contains a primitive
notion of equality, while leaving the notion of expansion proof
unaltered. This is possible, since a nonextensional equality is
definable in our system of type theory. Next we extend analytic and
nonanalytic proof systems and the translations between them to
include extensionality. Finally, we show how the methods and notions
used so far apply to the problem of translating expansion proofs into
natural deductions. Much care is taken to specify this translation in
a modular way (through tactics) which leaves a large number of choices
and therefore a lot of room for heuristics to produce elegant natural
deductions. A practically very useful extension, called symmetric
simplification, produces natural deductions which make use of lemmas
and are often much more intuitive than the normal deductions which
would be created by earlier algorithms.",
paper = "Pfen87.pdf"
}\end{chunk}
\index{Comon, Hubert}
\begin{chunk}{ axiom.bib}
@incollection{Como01,
author = "Comon, Hubert",
title = {{Inductionless Induction}},
booktitle = "Handbook of Automated Reasoning",
comment = "Chapter 14",
publisher = "Elsevier",
year = "2001",
paper = "Como01.ps"
}\end{chunk}
\index{Schmitt, P.H.}
\begin{chunk}{ axiom.bib}
@article{Schm86,
author = "Schmitt, P.H.}",
title = {{Computational Aspects of ThreeValued Logic}},
journal = "LNCS",
volume = "230",
year = "1986",
abstract =
"This paper investigates a threevalued logic $L_3$, that has been
introduced in the study of natural language semantics. A complete
proof system based on a threevalued analogon of negative resolution
is presented. A subclass of $L_3$ corresponding to Horn clauses in
twovalued logic is defined. Its model theoretic properties are
studied and it is shown to admit a PROLOGstyle proof procedure.",
paper = "Schm86.pdf"
}\end{chunk}
\index{Common, Hubert}
\index{Lescanne, Pierre}
\begin{chunk}{ axiom.bib}
@article{Como89,
author = "Common, Hubert and Lescanne, Pierre",
title = {{Equational Problems and Disunification}},
journal = "J. Symbolic Computation",
volume = "7",
number = "34",
year = "1989",
pages = "371425",
abstract =
"Roughly speaking, an equational problem is a first order formula
whose only predicate symbol is $=$. We propose some rules for the
transformation of equational problems and study their correctness in
various models. Then, we give completeness results with respect to
some 'simple' problems called solved forms. Such completeness results
still hold when adding some control which moreover ensures
termination. The termination proofs are given for a 'weak' control and
thus hold for the (large) class of algorithms obtained by restricting
the scope of the rules. Finally, it must be noted that a byproduct of
our method is a decision procedure for the validity in the Herbrand
Universe of any first order formula with the only predicate symbol $=$.",
paper = "Como89.pdf"
}\end{chunk}
\index{Jones, Simon > Peyton}
\begin{chunk}{ axiom.bib}
@inproceedings{Jone96,
author = "Jones, Simon > Peyton",
title = {{Compiling Haskell by Program Transformation: A Report from
the Trenches}},
booktitle = "Proc. European Symposium on Programming",
year = "1996",
publisher = "Eurographics",
abstract =
"Many compilers do some of their work by means of
correctnesspreseving, and hopefully performance improving, program
transformations. The Glasgow Haskell Compiler (GHC) takes this idea
of 'compilation by transformation' as its warcry, trying to express
as much as possible of the compilation process in the form of
program transformations.This paper reports on our practical experience of the
transformational approach to compilation, in the context of a
substantial compiler.",
paper = "Jone96.pdf"
}\end{chunk}
\index{Hanus, Michael}
\begin{chunk}{ axiom.bib}
@article{Hanu90,
author = "Hanus, Michael",
title = {{Compiling Logic Programs with Equality}},
journal = "LNCS",
volume = "456",
year = "1990",
pages = "387401",
abstract =
"Horn clause logic with equality is an amalgamation of functional and
logic programming languages. A sound and complete operational
semantics for logic programs with equality is based on resolution to
solve literals, and rewriting and narrowing to evaluate functional
expressions. This paper proposes a technique for compiling programs
with these inference rules into programs of a lowlevel abstract
machine which can be efficiently executed on conventional
architectures. The presented approach is based on an extension of the
Warren abstract machine (WAM). In our approach pure logic programs
without function definitions are compiled in the same way as in the
WAMapproach, and for logic programs with function definitions
particular instructions are generated for occurrences of functions
inside clause bodies. In order to obtain an efficient implementation
of functional computations, a stack of occurrences of function symbols
in goals is managed by the abstract machine. The compiler generates
the necessary instructions for the efficient manipulation of the
occurrence stack from the given equational logic programs.",
paper = "Hanu90.pdf"
}\end{chunk}
\index{Ballerin, Clemens}
\begin{chunk}{ axiom.bib}
@phdthesis{Ball99a,
author = "Ballerin, Clemens",
title = {{Computer Algebra and Theorem Proving}},
school = "Darwin College, University of Cambridge",
year = "1999",
abstract =
"Is the use of computer algebra technology beneficial for
mechanised reasoining in and about mathematical domains? Usually
it is assumed that it is. Many works in this area, however, either
have little reasoning conent, or use symbolic computation only to
simplify expressions. In work that has achieved more, the used
methods do not scale up. They trust the computer algebra system
either too much or too little.Computer algebra systems are not as rigorous as many provers. They
are not logically sound reasoning systems, but collections of
algorithms. We classify soundness problems that occur in computer
algebra systems. While many algorithms and their implementations
are perfectly trustworthy, the semantics of symbols is often
unclear and leads to errors. On the other hand, more robust
approaches to interface external reasoners to provers are not
always practical because the mathematical depth of proofs
algorithms in computer algebra are based on can be enormous.Our own approach takes both trustworthiness of the overall system
and efficiency into account. It relies on using only reliable
parts of a computer algebra system, which can be achieved by
choosing a suitable library, and deriving specifications for these
algorithms from their literature.We design and implement an interface between the prover Isabelle
and the computer algebra library Sumit and use it to prove
nontrivial theorems from coding theory. This is based on the
mechanisation of the algebraic theories of rings and
polynomials. Coding theory is an area where proofs do have a
substantial amount of computational content. Also, it is realistic
to assume that the verification of an encoding or decoding device
could be undertaken in, and indeed, be simplified by, such a
system.The reason why semantics of symbols is often unclear in current
computer algebra systems is not mathematical difficulty, but the
design of those systems. For Gaussian elimination we show how the
soundness problem can be fixed by a small extension, and without
losing efficiency. This is a prerequisite for the efficient use of
the algorithm in a prover.",
paper = "Ball99a.pdf",
keywords = "axiomref, printed"
}\end{chunk}
\index{Nederpelt, Rob}
\index{Geuvers, Nerman}
\begin{chunk}{ axiom.bib}
@book{Nede14,
author = "Nederpelt, Rob and Geuvers, Nerman",
title = {{Type Theory and Formal Proof}},
year = "2014",
publisher = "Cambridge University Press",
isbn = "9781107036505"
}\end{chunk}
\index{Robinson, Alan}
\index{Voronkov, Andrei}
\begin{chunk}{ axiom.bib}
@book{Robi01,
author = "Robinson, Alan and Voronkov, Andrei",
title = {{Handbook of Automated Reasoning (2 Volumes)}},
year = "2001",
publisher = "MIT Press",
isbn = "0262182238"
}\end{chunk}
\index{Barendregt, Henk}
\index{Wiedijk, Freek}
\begin{chunk}{ axiom.bib}
@article{Bare05,
author = "Barendregt, Henk and Wiedijk, Freek",
title = {{The Challenge of Computer Mathematics}},
journal = "Phil. Trans. Royal Society",
volume = "363",
pages = "23512375",
year = "2005",
abstract =
"Progress in the foundations of mathematics has made it possible to
formulate all thinkable mathematical concepts, algorithms and proofs
in one language and in an impeccable way. This is not in spite of, but
partially based on the famous results of Godel and Turing. In this way
statements are about mathematical objects and algorithms, proofs show
the correctness of statements and computations, and computations are
dealing with objects and proofs. Interactive computer systems for a
full integration of defining, computing and proving are based on
this. The human defines concepts, constructs algorithms and provides
proofs, while the machine checks that the definitions are well formed
and the proofs and computations are correct. Results formalized so far
demonstrate the feasibility of this ‘computer mathematics’. Also there
are very good applications. The challenge is to make the systems more
mathematicianfriendly, by building libraries and tools. The eventual
goal is to help humans to learn, develop, communicate, referee and
apply mathematics.",
paper = "Bare05.pdf",
keywords = "printed"
}\end{chunk}
\index{Klaeren, Herbert A.}
\begin{chunk}{ axiom.bib}
@article{Klae84,
author = "Klaeren, Herbert A.",
title = {{A Constructive Method for Abstract Algebraic Software
Specificat ion}},
journal = "Theoretical Computer Science",
vollume = "30",
year = "1984",
pages = "139204",
abstract =
"A constructive method for abstract algebraic software
specification is presented, where the operations are not
implicitly specified by equations but by an explicit recursion on
the generating operations of an algebra characterizing the
underlying data structure. The underlying algebra itself may be
equationally specified since we cannot assume that all data
structures will correspond to free algebras. This implies that we
distinguish between generating and defined operations and that the
underlying algebra has a mechanism of wellfounded decomposition
w.r.t. the generating operations. We show that the explicit
specification of operations using socalled structural recursive
schemata offers advantages over purely equational specifications,
especially concerning the safeness of enrichments, the ease of
semantics description and the separation between the underlying
data structure and the operations defined on it.",
keywords = "printed"
}\end{chunk}
\index{Pfenning, Frank}
\begin{chunk}{ axiom.bib}
@misc{Pfen04,
author = "Pfenning, Frank",
title = {{Automated Theorem Proving}},
year = "2004",
comment = "Draft of Spring 2004",
keywords = "printed"
}\end{chunk}
\index{Coquuand, Thierry}
\index{Huet, Gerard}
\begin{chunk}{ axiom.bib}
@incollection{Coqu88,
author = "Coquuand, Thierry and Huet, Gerard",
title = {{The Calculus of Constructions}},
booktitle = "Information and Computation, Volume 76",
year = "1988",
publisher = "Academic Press",
paper = "Coqu88.pdf",
keywords = "printed"
}\end{chunk}
\index{Okasaki, Chris}
\begin{chunk}{ axiom.bib}
@phdthesis{Okas96,
author = "Okasaki, Chris",
title = {{Purely Functional Data Structures}},
school = "Carnegie Mellon University",
year = "1996",
link = "\url{}",
comment = "CMUCS96177",
isbn = "9780521663502",
abstract =
"When a C programmer needs an efficient data structure for a
particular problem, he or she can often simply look one up in any of
a number of good textbooks or handbooks. Unfortunately, programmers
in functional languages such as Standard ML or Haskell do not have
this luxury. Although some data structures designed for imperative
languages such as C can be quite easily adapted to a functional
setting, most cannot, usually because they depend in crucial ways on
assignments, which are disallowed, or at least discouraged, in
functional languages. To address this imbalance, we describe several
techniques for designing functional data structures, and numerous
original data structures based on these techniques, including multiple
variations of lists, queues, doubleended queues, and heaps, many
supporting more exotic features such as random access or efficient
catenation.In addition, we expose the fundamental role of lazy evaluation in
amortized functional data structures. Traditional methods of
amortization break down when old versions of a data structure, not
just the most recent, are available for further processing. This
property is known as persistence , and is taken for granted in
functional languages. On the surface, persistence and amortization
appear to be incompatible, but we show how lazy evaluation can be used
to resolve this conflict, yielding amortized data structures that are
efficient even when used persistently. Turning this relationship
between lazy evaluation and amortization around, the notion of
amortization also provides the first practical techniques for
analyzing the time requirements of nontrivial lazy programs.Finally, our data structures offer numerous hints to programming
language designers, illustrating the utility of combining strict and
lazy evaluation in a single language, and providing nontrivial
examples using polymorphic recursion and higherorder, recursive
modules.",
paper = "Okas96.pdf"
}\end{chunk}
\index{Letouzey, Pierre}
\begin{chunk}{ axiom.bib}
@inproceedings{Leto04,
author = "Letouzey, Pierre",
title = {{A New Extraction for Coq}},
booktitle = "Types for Proofs and Programs. TYPES 2002",
publisher = "Springer",
pages = "617635",
year = "2004",
abstract =
"We present here a new extraction mechanism for the Coq proof
assistant. By extraction, we mean automatic generation of
functional code from Coq proofs, in order to produce certified
programs. In former versions of Coq, the extraction mechanism
suffered several limitations and in particular worked only with a
subset of the language. We first discuss difficulties encountered
and solutions proposed to remove these limitations. Then we give a
proof of correctness for a theoretical model of the new
extraction. Finally we describe the actual implementation.",
paper = "Leto04.pdf",
keywords = "printed"
}\end{chunk}
\index{Abrams, Marshall D.}
\index{Zelkowitz, Marvin V.}
\begin{chunk}{ axiom.bib}
@article{Abra95,
author = "Abrams, Marshall D. and Zelkowitz, Marvin V.",
title = {{Striving for Correctness}},
journal = "Computers and Security",
volume = "14",
year = "1995",
pages = "719738",
paper = "Abra95.pdf"
}\end{chunk}
\index{Parnas, David L.}
\begin{chunk}{ axiom.bib}
@article{Parn72,
author = "Parnas, David L.",
title = {{A Technique for Software Module Specification with
Examples} },
journal = "CACM",
volume = "15",
number = "5",
year = "1972",
pages = "330336",
abstract =
"This paper presents an approach to writing specifications for
parts of software systems. The main goal is to provide
specifications sufficiently precise and complete that other pieces
of software can be written to interact with the piece specified
without additional information. The secondary goal is to include
in the specification no more information than necessary to meet
the first goal. The technique is illustrated by means of a variety
of examples from a tutorial system.",
paper = "Parn72.pdf",
keywords = "printed"
}\end{chunk}
\index{Johnson, C.W.}
\begin{chunk}{ axiom.bib}
@article{John96,
author = "Johnson, C.W.",
title = {{Literate Specifications}},
journal = "Software Engineering Journal",
volume = "11",
number = "4",
year = "1996",
pages = "225237",
paper = "John96.pdf",
abstract =
"The increasing scale and complexity of software is imposing serious
burdens on many industries. Formal notations, such as Z, VDM and
temporal logic, have been developed to address these problems. There
are, however, a number of limitations that restrict the use of
mathematical specifications far largescale software development. Many
projects take months or years to complete. This creates difficulties
because abstract mathematical requirements cannot easily be used by
new members of a development team to understand past design
decisions. Formal specifications describe what software must do, they
do not explain why it must do it. In order to avoid these limitations,
a literate approach to software engineering is proposed. This
technique integrates a formal specification language and a semiformal
design rationale. The Z schema calculus is usecl to represent what a
system must do. In contrast, the Questions, Options and Criteria
notation is used to represent the justifications that lie behind
development decisions. Empirical evidence is presented that suggests
the integration of these techniques provides significant benefits over
previous approaches to mathematical analysis and design techniques. A
range of tools is described that have been developed to support our
literate approach to the specification of largescale sohare systems.",
keywords = "printed"
}\end{chunk}
\index{Finney, Kate}
\begin{chunk}{ axiom.bib}
@article{Finn96,
author = "Finney, Kate",
title = {{Mathematical Notation in Formal Specifications: Too
Difficult for the Masses?}},
journal = "IEEE Trans. on Software Engineering",
volume = "22",
number = "2",
year = "1996",
pages = "158159",
abstract =
"The phrase 'not much mathematics required' can imply a
variety of skill levels. When this phrase is applied to computer
scientists, software engineers, and clients in the area of formal
specification, the word 'much' can be widely misinterpreted with
disastrous consequences. A small experiment in reading
specifications revealed that students already trained in discrete
mathematics and the specification notation performed very poorly;
much worse than could reasonably be expected if formal methods
proponents are to be believed.",
paper = "Finn96.pdf",
keywords = "printed"
}\end{chunk}
\index{Moore, Andrew P.}
\index{Payne Jr., Charles N.}
\begin{chunk}{ axiom.bib}
@inproceedings{Moor96,
author = "Moore, Andrew P. and Payne Jr., Charles N.",
title = {{Increasing Assurance with LIterate Programming Techniques}},
booktitle = "Comf. on Computer Assurance COMPASS'96",
publisher = "National Institute of Standards and Technology",
year = "1996",
pages = "187198",
abstract =
"The assurance argument that a trusted system satisfies its
information security requirements must be convincing, because the
argument supports the accreditation decision to allow the computer to
process classified information in an operational
environment. Assurance is achieved through understanding, but some
evidence that supports the assurance argument can be difficult to
understand. This paper describes a novel applica tion of a technique,
called literate programming [ll], that significantly improves the
readability of the assur ance argument while maintaining its
consistency with formal specifications that are input to specification
and verification systems. We describe an application c,f this
technique to a simple example and discuss the lessons learned from
this effort.",
paper = "Moor96.pdf",
keywords = "printed"
}\end{chunk}
\index{Nissanke, Nimal}
\begin{chunk}{ axiom.bib}
@book{Niss99,
author = "Nissanke, Nimal",
title = {{Formal Specification}},
publisher = "Springer",
year = "1999",
isbn = "978185233002 6",
paper = "Niss99.pdf"
}\end{chunk}
\index{Vienneau, Robert L.}
\begin{chunk}{ axiom.bib}
@misc{Vien93,
author = "Vienneau, Robert L.",
title = {{A Review of Formal Methods}},
year = "1993",
paper = "Vien93.pdf",
keywords = "printed"
}\end{chunk}
\index{Murthy, S.G.K}
\index{Sekharam, K. Raja}
\begin{chunk}{ axiom.bib}
@article{Murt09,
author = "Murthy, S.G.K and Sekharam, K. Raja",
title = {{Software Reliability through Theorem Proving}},
journal = "Defence Science Journal",
volume = "59",
number = "3",
year = "2009",
pages = "314317",
abstract =
"Improving software reliability of missioncritical systems is
widely recognised as one of the major challenges. Early detection
of errors in software requirements, designs and implementation,
need rigorous verification and validation techniques. Several
techniques comprising static and dynamic testing approaches are
used to improve reliability of mission critical software; however
it is hard to balance development time and budget with software
reliability. Particularly using dynamic testing techniques, it is
hard to ensure software reliability, as exhaustive testing is not
possible. On the other hand, formal verification techniques
utilise mathematical logic to prove correctness of the software
based on given specifications, which in turn improves the
reliability of the software. Theorem proving is a powerful formal
verification technique that enhances the software reliability for
mission critical aerospace applications. This paper discusses the
issues related to software reliability and theorem proving used to
enhance software reliability through formal verification
technique, based on the experiences with STeP tool, using the
conventional and internationally accepted methodologies, models,
theorem proving techniques available in the tool without proposing
a new model.",
paper = "Murt09.pdf",
keywords = "printed"
}\end{chunk}
\index{Paulson, Lawrence C.}
\begin{chunk}{ axiom.bib}
@incollection{Paul90a,
author = "Paulson, Lawrence C.",
title = {{Isabelle: The Next 700 Theorem Provers}},
booktitle = "Logic and Computer Science",
publisher = "Academic Press",
pages = "361386",
year = "1990",
paper = "Paul90a.pdf"
}\end{chunk}
\index{Beeson, M.}
\begin{chunk}{ axiom.bib}
@article{Bees16,
author = "Beeson, M.",
title = {{Mixing Computations and Proofs}},
journal = "J. of Formalized Reasoning",
volume = "9",
number = "1",
pages = "7199",
year = "2016",
abstract =
"We examine the relationship between proof and computation in
mathematics, especially in formalized mathematics. We compare the
various approaches to proofs with a significant computational
component, including (i) verifying the algorithms, (ii) verifying the
results of the unverified algo rithms, and (iii) trusting an external
computation.",
paper = "Bees16.pdf",
keywords = "printed"
}\end{chunk}
\index{Beeson, Michael}
\begin{chunk}{ axiom.bib}
@misc{Bees14,
author = "Beeson, M.",
title = {{Mixing Computations and Proofs}},
comment = "slides",
year = "2014",
link = "\url{http://www.cs. }",ru.nl/qed20/ slides/ beeson qed20.pdf
paper = "Bees14.pdf"
}\end{chunk}
\index{Gunter, Elsa L.}
\begin{chunk}{ axiom.bib}
@inproceedings{Gunt89a,
author = "Gunter, Elsa L.",
booktitle = "Int. Workshop on Extensions of Logic Programming",
publisher = "Springer",
year = "1989",
pages = "223244",
abstract =
"In this article, we discuss several possible extensions to
traditional logic programming languages. The specific extensions
proposed here fall into two categories: logical extensions and the
addition of constructs to allow for increased control. There is a
unifying theme to the proposed logical extensions, and that is the
scoped introduction of extensions to a programming context. More
specifically, these extensions are the ability to introduce variables
whose scope is limited to the term in which they occur (i.e. Abound
variables within Aterms), the ability to intro~iuce into a goal a
fresh constant whose scope is limited to the derivation of that goal,
and the ability to introduce into a goal a program clause whose scope
is limited to the derivation of that goal. The purpose of the
additions for increased control is to facilitate the raising and
handling of failures.To motivate these various extensions, we have repeatedly appealed to
examples related to the construction of a generic theorem prover. It
is our thesis that this problem domain is specific enough to lend
focus when one is considering various language constructs, and yet
complex enough to encompass many of the general difficulties found in
other areas of symbolic computation.",
paper = "Gunt89a.pdf"
}\end{chunk}
\index{Paulson, Lawrence C.}
\index{Smith, Andrew W.}
\begin{chunk}{ axiom.bib}
@inproceedings{Paul89,
author = "Paulson, Lawrence C. and Smith, Andrew W.",
title = {{Logic Programming, Functional Programming, and
Inductive Definitions}},
booktitle = "Int. Workshop on Extensions of Logic Programming",
publisher = "Springer",
year = "1989",
pages = "283309",
abstract =
"The unification of logic and functional programming, like the Holy
Grail, is sought by countless people [6, 14]. In reporting our
attempt, we first discuss the motivation. We argue that logic
programming is still immature, compared with functional programming,
because few logic programs are both useful and pure. Functions can
help to purify logic programming, for they can eliminate certain uses
of the cut and can express certMn negations positively.More generally, we suggest that the traditional paradigm  logic
programming as firstorder logic  is seriously out of step with
practice. We offer an alternative paradigm. We view the logic program
as an inductive definition of sets and relations. This view explains
certain uses of Negation as Failure, and explains why most attempts to
extend PROLO G to larger fragments of firstorder logic have not been
successful. It suggests a logic language with functions,
incorporating equational unification.We have implemented a prototype of this language. It is very slow,
but complete, and appear to be faster than some earlier
implementations of narrowing. Our experiments illustrate the
programming style and shed light on the further development of such
languages.",
paper = "Paul89.pdf"
}\end{chunk}
\index{Weirich, Jim}
\begin{chunk}{ axiom.bib}
@misc{Weir12,
author = "Weirich, Jim",
title = {{Y Not?  Adventures in Functional Programming}},
year = "2012",
link = "\url{https://www.infoq. }",com/presentatio ns/YCombinator
abstract = "Explains the YCombinator"
}\end{chunk}
\index{Beeson, Michael}
\begin{chunk}{ axiom.bib}
@article{Bees06,
author = "Beeson, Michael",
title = {{Mathematical Induction in OtterLambda}},
journal = "J. Automated Reasoning",
volume = "36",
number = "4",
pages = "311'344",
abstract =
"Otterlambda is Otter modified by adding code to implement an
algorithm for lambda unification. Otter is a resolutionbased,
clauselanguage firstorder prover that accumulates deduced clauses
and uses strategies to control the deduction and retention of
clauses. This is the first time that such a firstorder prover has
been combined in one program with a unification algorithm capable of
instantiating variables to lambda terms to assist in the
deductions. The resulting prover has all the advantages of the
proofsearch algorithm of Otter (speed, variety of inference rules,
excellent handling of equality) and also the power of lambda
unification. We illustrate how these capabilities work well together
by using Otterlambda to find proofs by mathematical induction. Lambda
unification instantiates the induction schema to find a useful
instance of induction, and then Otter's firstorder reasoning can be
used to carry out the base case and induction step. If necessary,
induction can be used for those, too. We present and discuss a variety
of examples of inductive proofs found by Otterlambda: some in pure
Peano arithmetic, some in Peano arithmetic with defined predicates,
some in theories combining algebra and the natural numbers, some
involving algebraic simplification (used in the induction step) by
simplification code from MathXpert, and some involving list induction
instead of numerical induction. These examples demonstrate the
feasibility and usefulness of adding lambda unification to a
firstorder prover.",
papers = "Bees06.pdf",
keywords = "printed"
}\end{chunk}
\index{Barendregt, Henk}
\index{Barendsen, Erik}
\begin{chunk}{ axiom.bib}
@article{Bare02,
author = "Barendregt, Henk and Barendsen, Erik",
title = {{Autorkic Computations in Formal Proofs}},
journal = "J. Automated Reasoning",
volume = "28",
pages = "321336",
year = "2002",
abstract =
"Formal proofs in mathematics and computer science are being studied
because these objects can be verified by a very simple computer
program. An important open problem is whether these formal proofs can
be generated with an effort not much greater than writing a
mathematical paper in, say, LATEX. Modern systems for proof
development make the formalization of reasoning relatively
easy. However, formalizing computations in such a manner that the
results can be used in formal proofs is not immediate. In this paper
we show how to obtain formal proofs of statements such as Prime(61) in
the context of Peano arithmetic or $(x + 1)(x + 1) = x 2 + 2x + 1$ in
the context of rings. We hope that the method will help bridge the gap
between the efficient systems of computer algebra and the reliable
systems of proof development.",
paper = "Bare02.pdf",
keywords = "printed"
}\end{chunk}
\index{Beeson, Michael}
\begin{chunk}{ axiom.bib}
@article{Bees95,
author = "Beeson, Michael",
title = {{Using Nonstandard Analysis to Ensure the Correctness of
Symbolic Computations}},
journal = "Int. J. of Foundations of Computer Science",
volume = "6",
number = "3",
pages = "299338",
year = "1995",
abstract =
"Nonstandard analysis has been put to use in a theoremprover,
where it assists in the analysis of formulae involving limits. The
theoremprover in question is used in the computer program
Mathpert to ensure the correctness of calculations in
calculus. Although nonstandard analysis is widely viewed as
nonconstructive, it can alternately be viewed as a method of
reducing logical manipulation (of formulae with quantifiers) to
coputation (with rewrite rules). We give a logical theory of
nonstandard analysis which is implemented in Mathpert. We describe
a procedure for 'elimination of infinitesimals' (also implemented
in Mathpert) and prove its correctness.",
paper = "Bees95.pdf",
keywords = "printed"
}\end{chunk}
\index{Beeson, Michael}
\index{Wiedijk, Freek}
\begin{chunk}{ axiom.bib}
@article{Bees02,
author = "Beeson, Michael and Wiedijk, Freek",
title = {{The Meaning of Infinity in Calculus and Computer Algebra
Systems} },
journal = "LNCS",
volume = "2385",
year = "2002",
abstract =
"We use filters of open sets to provide a semantics justifying the
use of infinity in informal limit calculations in calculus, and in
the same kind of calculations in computer algebra. We compare the
behavior of these filters to the way Mathematica behaves when
calculating with infinity.We stress the need to have a proper semantics for computer algebra
expressions, especially if one wants to use results and methods
from computer algebra in theorem provers. The computer algebra
method under discussion in this paper is the use of rewrite rules
to evaluate limits involving infinity.",
paper = "Bees02.pdf",
keywords = "printed"
}\end{chunk}
\index{Zimmer, Jurgen}
\index{Dennis, Louise A.}
\begin{chunk}{ axiom.bib}
@article{Zimm02,
author = "Zimmer, Jurgen and Dennis, Louise A.",
title = {{Inductive Theorem Proving and Computer Algebra in the
MathWeb Software Bus}},
journal = "LNCS",
volume = "2385",
year = "2002",
abstract =
"Reasoning systems have reached a high degree of maturity in the last
decade. However, even the most successful systems are usually not
general purpose problem solvers but are typically specialised on
problems in a certain domain. The MathWeb Software Bus (MathWebSB) is a
system for combining reasoning specialists via a common software bus.
We describe the integration of the $\lambda$Clam system, a reasoning
specialist for proofs by induction, into the MathWebSB. Due to this
integration, $\lambda$Clam now offers its theorem proving expertise
to other systems in the MathWebSB. On the other hand,
$\lambda$Clam can use the
services of any reasoning specialist already integrated. We focus on
the latter and describe first experiments on proving theorems by
induction using the computational power of the Maple system within
$\lambda$Clam." ,
paper = "Zimm02.pdf",
keywords = "printed"
}\end{chunk}
\index{Campbell, J.A.}
\begin{chunk}{ axiom.bib}
@article{Camp02,
author = "Campbell, J.A.",
title = {{Indefinite Integration as a Testbed for Developments in
Multi agent Systems}},
journal = "LNCS",
volume = "2385",
year = "2002",
abstract =
"Coordination of multiple autonomous agents to solve problems that
require each of them to contribute their limited expertise in the
construction of a solution is often ensured by the use of numerical
methods such as votecounting, payoff functions, game theory and
economic criteria. In areas where there are no obvious numerical methods
for agents to use in assessing other agents’ contributions, many
questions still remain open for research. The paper reports a study of
one such area: heuristic indefinite integration in terms of agents with
different single heuristic abilities which must cooperate in finding
indefinite integrals. It examines the reasons for successes and lack
of success in performance, and draws some general conclusions about
the usefulness of indefinite integration as a field for realistic
tests of methods for multiagent systems where the usefulness of
'economic' criteria is limited. In this connection, the role of
numerical taxonomy is emphasised.",
paper = "Camp02.pdf",
keywords = "printed"
}\end{chunk}
\index{Wiedijk, Freek}
\begin{chunk}{ axiom.bib}
@misc{Wied18,
author = "Wiedijk, Freek",
title = {{Formaizing 100 Theorems}},
link = "\url{http://www.cs. }",ru.nl/~ freek/100/
year = "2018"
}\end{chunk}
\index{Wiedijk, Freek}
\begin{chunk}{ axiom.bib}
@misc{Wied08,
author = "Wiedijk, Freek",
title = {{Formai Proof  Geting Started}},
link = "\url{https://www.ams. }",org/notices/ 200811/ tx081101408p. pdf
year = "2008",
paper = "Wied08.pdf"
}\end{chunk}
\index{Kaliszyk, Cezary}
\begin{chunk}{ axiom.bib}
@article{Kali08,
author = "Kaliszyk, Cezary",
title = {{Automating Side Conditions in Formalized Partial Functions}},
journal = "LNCS",
volume = "5144",
year = "2008",
abstract =
"Assumptions about the domains of partial functions are necessary in
stateofthe art proof assistants. On the other hand when
mathematicians write about partial functions they tend not to
explicitly write the side conditions. We present an approach to
formalizing partiality in real and complex analysis in total
frameworks that allows keeping the side conditions hidden from the
user as long as they can be computed and simplified
automatically. This framework simplifies defining and operating on
partial functions in formalized real analysis in HOL Light. Our
framework allows simplifying expressions under partiality conditions
in a proof assistant in a manner that resembles computer algebra
systems.",
paper = "Kali08.pdf"
}\end{chunk}
\index{Kaliszyk, Cezary}
\index{Wiedijk, Freek}
\begin{chunk}{ axiom.bib}
@article{Kali08a,
author = "Kaliszyk, Cezary and Wiedijk, Freek",
title = {{Merging Procedural and Declarative Proof}},
journal = "LNCS",
volume = "5497",
year = "2008",
abstract =
"There are two different styles for writing natural deduction proofs:
the 'Gentzen' style in which a proof is a tree with the conclusion at
the root and the assumptions at the leaves, and the 'Fitch' style
(also called ‘flag’ style) in which a proof consists of lines that are
grouped together in nested boxes.In the world of proof assistants these two kinds of natural deduction
correspond to procedural proofs (tactic scripts that work on one or
more subgoals, like those of the Coq, HOL and PVS systems), and
declarative proofs (like those of the Mizar and Isabelle/Isar
languages).In this paper we give an algorithm for converting tree style proofs to
flag style proofs. We then present a rewrite system that simplifies
the results.This algorithm can be used to convert arbitrary procedural proofs to
declarative proofs. It does not work on the level of the proof terms
(the basic inferences of the system), but on the level of the
statements that the user sees in the goals when constructing the
proof.The algorithm from this paper has been implemented in the ProofWeb
interface to Coq. In ProofWeb a proof that is given as a Coq proof
script (even with arbitrary Coq tactics) can be displayed both as a
tree style and as a flag style proof.",
paper = "Kali08a.pdf",
keywords = "printed"
}\end{chunk}
\index{Akbarpour, Behzad}
\index{Paulson, Lawrence C.}
\begin{chunk}{ axiom.bib}
@article{Akba08a,
author = "Akbarpour, Behzad and Paulson, Lawrence C.",
title = {{MetiTarski: An Automatic Prover for the Elementary Functions}},
journal = "LNCS",
volume = "5144",
year = "2008",
abstract =
"Many inequalities involving the functions ln, exp, sin, cos, etc.,
can be proved automatically by MetiTarski: a resolution theorem prover
(Metis) modified to call a decision procedure (QEPCAD) for the theory
of real closed fields. The decision procedure simplifies clauses by
deleting literals that are inconsistent with other algebraic facts,
while deleting as redundant clauses that follow algebraically from
other clauses. MetiTarski includes special code to simplify
arithmetic expressions.",
paper = "Akba08a.pdf"
}\end{chunk}
\index{Cramer, Marcos}
\begin{chunk}{ axiom.bib}
@misc{Cram14,
author = "Cramer, Marcos",
title = {{Modelling the usage of partial functions and undefined
terms using presupposition theory}},
year = "2014",
isbn = "978184890130 8",
publisher = "College Publications",
pages = "7188",
abstract =
"We describe how the linguistic theory of presuppositions can be used
to analyse and model the usage of partial functions and undefined
terms in mathematical texts. We compare our account to other accounts
of partial functions and undefined terms, showing how our account
models the actual usage of partial functions and undefined terms more
faithfully than existing accounts. The model described in this paper
has been developed for the Naproche system, a computer system for
proofchecking mathematical texts written in controlled natural
language, and has largely been implemented in this system.",
paper = "Cram14.pdf",
keywords = "printed"
}\end{chunk}
\index{Freundt, Sebastian}
\index{Horn, Peter}
\index{Konovalov, Alexander}
\index{Linton, Steve}
\index{Roozemond, Dan}
\begin{chunk}{ axiom.bib}
@article{Freu08,
author = "Freundt, Sebastian and Horn, Peter and Konovalov, Alexander
and Linton, Steve and Roozemond, Dan",
title = {{Symbolic Computation Software Composability}},
journal = "LNCS",
volume = "5144",
year = "2008",
abstract =
"We present three examples of the composition of Computer Algebra
Systems to illustrate the progress on a composability infrastructure
as part of the SCIEnce (Symbolic Computation Infrastructure for
Europe) project 1 . One of the major results of the project so far is
an OpenMath based protocol called SCSCP (Symbolic Computation Software
Composability Protocol). SCSCP enables the various software packages
for example to exchange mathematical objects, request calcula tions,
and store and retrieve remote objects, either locally or accross the
internet. The three examples show the current state of the GAP, KANT,
and MuPAD software packages, and give a demonstration of exposing
Macaulay using a newly developed framework.",
paper = "Freu08.pdf",
keywords = "printed"
}\end{chunk}
\index{Kozen, Dexter}
\index{Palsberg, Jens}
\index{Schwartzbach, Michael I.}
\begin{chunk}{ axiom.bib}
@article{Koze93,
author = "Kozen, Dexter and Palsberg, Jens and Schwartzbach, Michael I.",
title = {{Efficient Recursive Subtyping}},
journal = "Mathematical Structures in Computer Science",
volume = "5",
number = "1",
pages = "113125",
year = "1995",
abstract =
"Subtyping in the presence of recursive types for the
$\lambda$calculus was studied by Amadio and Cardelli in 1991. In that
paper they showed that the problem of deciding whether one recursive
type is a subtype of another is decidable in exponential time. In
this paper we give an $O(n^2)$ algorithm. Our algorithm is based on a
simplification of the definition of the subtype relation, which allows
us to reduce the problem to the emptiness problem for a certain finite
automaton with quadratically many states. It is known that equality
of recursive types and the covariant B̈ohm order can be decided
efficiently by means of finite automata, since they are just language
equality and language inclusion, respectively. Our results extend the
automatatheoretic approach to handle orderings based on
contravariance.",
paper = "Koze93.pdf"
}\end{chunk}
\index{Martelli, Alberto}
\index{Montanari, Ugo}
\begin{chunk}{ axiom.bib}
@article{Mart82,
author = "Martelli, Alberto and Montanari, Ugo",
title = {{An Efficient Unification Algorithm}},
journal = "ACM TOPLAS",
volume = "4",
number = "2",
pages = "258282",
year = "1982",
abstract =
"The unification problem in firstorder predicate calculus is
described in general terms as the solution of a system of equations,
and a nondeterministic algorithm is given. A new unification
algorithm, characterized by having the acyclicity test efficiently
embedded into it, is derived from the nondeterministic one, and a
PASCAL implementation is given. A comparison with other wellknown
unification algorithms shows that the algorithm described here
performs well in all cases.",
paper = "Mart82.pdf"
}\end{chunk}
\index{Pottier, Francois}
\begin{chunk}{ axiom.bib}
@phdthesis{Pott98,
author = "Pottier, Francois",
title = {{Type Inference in the Presence of Subtyping: From Theory
to Practice}},
school = "Universite Paris 7",
year = "1988",
comment = "INRIA Research Report RR3483",
abstract =
"From a purely theoretical point of view, type inference for a
functional language with parametric polymorphism and subtyping
poses little difficulty. Indeed, it suffices to generalize the
inference algorithm used in the ML language, so as to deal with
type inequalities, rather than equalities. However, the number of
such inequalities is linear in the program size  whence, from a
practical point of view, a serious efficiency and readability
problem.To solve this problem, one must simplify the inferred
constraints. So, after studying the logical properties of
subtyping constraints, this work proposes several simplifcation
algorithms. They combine seamlessly, yielding a homogeneous, fully
formal framework, which directly leads to an efficient
implementation. Although this theoretical study is performed in a
simplified setting, numerous extensions are possible. Thus, this
framework is realistic and should allow a practical appearance of
subtyping in languages with type inference.",
paper = "Pott98.pdf"
}\end{chunk}
\index{McCarthy, John}
\begin{chunk}{ axiom.bib}
@article{Mcca60,
author = "McCarthy, John",
title = {{Recursive Functions of Symbolic Expressions and Their
Computatio n by Machine, Part I}},
journal = "CACM",
volume = "3",
pages = "184195",
year = "1960",
paper = "Mcca60.pdf",
keywords = "printed"
}\end{chunk}
\index{Barendregt, Henk}
\begin{chunk}{ axiom.bib}
@incollection{Bare92,
author = "Barendregt, Henk",
title = {{Lambda Calculi with Types}},
booktitle = "Handbook of Logic in Computer Science (vol 2)",
publisher = "Oxford University Press",
year = "1992",
paper = "Bare92.pdf"
}\end{chunk}
\index{Church, Alonzo}
\begin{chunk}{ axiom.bib}
@article{Chur28,
author = "Church, Alonzo",
title = {{On the Law of the Excluded Middle}},
journal = "Bull. of the American Mathematical Society",
volume = "34",
number = "1",
pages = "7578",
year = "1928",
paper = "Chur28.pdf"
}\end{chunk}
\index{Mitchell, John}
\begin{chunk}{ axiom.bib}
@inproceedings{Mitc84
author = "Mitchell, John",
title = {{Type Inference and Type Containment}},
booktitle = "Proc. Int. Symp. on Semantics of Data Types",
publisher = "Springer",
isbn = "3540133461",
year = "1984"
pages = "257277",
abstract =
"Type inference, the process of assigning types to untyped
expressions, may be motivated by the design of a typed language or
semantical considerations on the meeaaings of types and expressions.
A typed language GR with polymorphic functions leads to the GR
inference rules. With the addition of an 'oracle' rule for equations
between expressions, the GR rules become complete for a general class
of semantic models of type inference. These inference models are
models of untyped lambda calculus with extra structure similar to
models of the typed language GR. A more specialized set of type
inference rules, the GRS rules, characterize semantic typing when the
functional type $a~$ , is interpreted as all elements of the model that
map a to $~r$ and the polymorphic type $Vt,~0$ is interpreted as the
intersection of all $o'(r)$. Both inference systems may be reformulated
using rules for deducing containments between types. The advantage of
the type inference rules based on containments is thatproofs
correspond more closely to the structure of terms.",
paper = "Mitc84.pdf"
}\end{chunk}
\index{Griesmer, James}
\begin{chunk}{ axiom.bib}
@artcile{Grie11,
author = "Griesmer, James",
title = {{James Griesmer 19292011}},
journal = "ACM Communications in Computer Algebra",
volume = "46",
number = "1/2",
year = "2012",
pages = "1011",
comment = "Obituary",
paper = "Grie11.pdf"
}\end{chunk}
\index{Daly, Timothy}
\index{Kastner, John}
\index{Mays, Eric}
\begin{chunk}{ axiom.bib}
@inproceedings{Daly88,
author = "Daly, Timothy and Kastner, John and Mays, Eric",
title = {{Integrating Rules and Inheritance Networks in a Knowlegebased
Financial Marketing Consutation System}},
booktitle = "Proc. HICSS 21",
volume = "3",
number = "58",
pages = "496500",
year = "1988",
comment = "KROPS",
abstract =
"This paper describes the integrated use of rulebascd inference and
an objectcentered knowledge representation (inheritance network) in a
financial marketing consultation system. The rules provide a highly
flexible pattern match capability and inference cycle for control. The
inheritance network provides a convenient way to represent the
conceptual structure of the domain. By merging the two techniques, our
financial computation can he shared at the most general level, and
rule inference is carried out at any appropriate Ievel of
generalization. Since domain knowledge is representcd independently
from control knowledge, knowledge ahout a particular problcm solving
technique is decoupled from the conditions for its invocation. A Iarge
financial marketing system has been built and examples are given to
show our combined use of rules and inheritance networks.",
paper = "Daly88.pdf"
}\end{chunk}
 2870. By daly on 20180516

books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Walther, J.S.}
\begin{chunk}{ axiom.bib}
@misc{Walt71,
author = "Walther, J.S.",
title = {{A Unified Algorithm for Elementary Functions}},
link = "\url{}",
year = "1971",
abstract =
"This paper describes a single unified algorithm for the calculation
of elementary functions including multipli cation, division, sin,
cos, tan, arctan, sinh, cosh, tanh, arctanh, In, exp and squareroot.
The basis for the algorithm is coordinate rotation in a linear,
circular, or hyperbolic coordinate system depending on which function
is to be calculated. The only operations re quired are shifting,
adding, subtracting and the recall of prestored constants. The
limited domain of con vergence of the algorithm is calculated,
leading to a discussion of the modifications required to extend the
domain for floating point calculations.A hardware floating point processor using the algo rithm was built at
HewlettPackard Laboratories. The block diagram of the processor, the
microprogram control used for the algorithm, and measures of actual
performance are shown.",
paper = "Walt71.pdf"
}\end{chunk}
\index{Friedman, Daniel P.}
\index{Wise, David S.}
\begin{chunk}{ axiom.bib}
@techreport{Frie76,
author = "Friedman, Daniel P. and Wise, David S.",
title = {{CONS should not Evaluate its Arguments}},
institution = "Indiana University",
number = "TR44",
year = "1976",
abstract =
"The constructor function which allocates and fills records in
recursive, sideeffectfree procedural languages is redefined to be a
nonstrict (Vuillemin 1974) elementary operation. Instead of
evaluating its arguments, it builds suspensions of them which are not
coerced until the suspensions is accessed by strict elementary
function. The resulting evalutation procedures are strictly more
powerful than existing schemes for languages such as LISP. The main
results are that Landin's streams are subsumed into McCarthy's LISP
merely by the redefinition of elementar functions, that invocations of
LISP's evaluator can be minimized by redefining the elemntary
functions without redefining the interpreter, and as a strong
conjecture, that redefining the elementary functions yields the least
fixedpoint semantics for McCarthy's evalution scheme. This new
insight into the role of construction functions will do much to ease
the interface between recursive programmers and iterative programmers,
as well as the interface between programmers and data structure
designers.",
paper = "Frie16.pdf",
keywords = "printed"
}\end{chunk}
\index{Sarma, Gopal}
\index{Hay, Nick J.}
\begin{chunk}{ axiom.bib}
@article{Sarm17,
author = "Sarma, Gopal and Hay, Nick J.",
title = {{Robust Computer Algebra, Theorem Proving, and Oracle AI}},
journal = "Informatica",
volume = "41",
number = "3",
link = "\url{https://arxiv. }",org/pdf/ 1708.02553. pdf
year = "2017",
abstract =
"In the context of superintelligent AI systems, the term 'oracle' has
two meanings. One refers to modular systems queried for
domainspecific tasks. Another usage, referring to a class of systems
which may be useful for addressing the value alignment and AI control
problems, is a superintelligent AI system that only answers questions.
The aim of this manuscript is to survey contemporary research problems
related to oracles which align with longterm research goals of AI
safety. We examine existing question answering systems and argue that
their high degree of architectural heterogeneity makes them poor
candidates for rigorous analysis as oracles. On the other hand, we
identify computer algebra systems (CASs) as being primitive examples
of domainspecific oracles for mathematics and argue that efforts to
integrate computer algebra systems with theorem provers, systems which
have largely been developed independent of one another, provide a
concrete set of problems related to the notion of provable safety that
has emerged in the AI safety community. We review approaches to
interfacing CASs with theorem provers, describe welldefined
architectural deficiencies that have been identified with CASs, and
suggest possible lines of research and practical software projects for
scientists interested in AI safety.",
paper = "Sarm17.pdf",
keywords = "printed, axiomref"
}\end{chunk}
\index{Keller, Chantal}
\begin{chunk}{ axiom.bib}
@phdthesis{Kell13,
author = "Keller, C.",
title = {{A Matter of Trust: Skeptical Commuication Between Coq and
External Provers}},
school = "Ecole Polytechnique",
year = "2013",
link =
"\url{https://www.lri. }",fr/~keller/ Documents recherche/ Publications/ thesis13. pdf
abstract =
"This thesis studies the cooperation between the Coq proof assistant
and external provers through proof witnesses. We concentrate on two
different kinds of provers that can return certicates: first, answers
coming from SAT and SMT solvers can be checked in Coq to increase both
the confidence in these solvers and Coq 's automation; second,
theorems established in interactive provers based on HigherOrder
Logic can be exported to Coq and checked again, in order to offer the
possibility to produce formal developments which mix these two
different logical paradigms. It ended up in two software : SMTCoq, a
bidirectional cooperation between Coq and SAT/SMT solvers, and
HOLLIGHTCOQ, a tool importing HOL Light theorems into Coq.For both tools, we took great care to define a modular and efficient
architecture, based on three clearly separated ingredients: an
embedding of the formalism of the external tool inside Coq which is
carefully translated into Coq terms, a certified checker to establish
the proofs using the certicates and a Ocaml preprocessor to transform
proof witnesses coming from different provers into a generic
certificate. This division allows that a change in the format of proof
witnesses only affects the preprocessor, but no proved Coq code.
Another fundamental component for efficiency and modularity is
computational reflection, which exploits the computational power of
Coq to establish generic and small proofs based on the certicates.",
paper = "Kell13.pdf"
}\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@article{Farm07,
author = "Farmer, William M.",
title = {{Biform Theories in Chiron}},
journal = "LNCS",
volume = "4573",
pages = "6679",
year = "2007",
abstract =
"An axiomatic theory represents mathematical knowledge declaratively
as a set of axioms. An algorithmic theory represents mathematical
knowledge procedurally as a set of algorithms. A biform theory is
simultaneously an axiomatic theory and an algorithmic theory. It
represents mathematical knowledge both declaratively and procedurally.
Since the algorithms of algorithmic theories manipulate th e syntax of
expressions, biform theories — as well as algorithmic theories — are
difficult to formalize in a traditional logic without the means to
reason about syntax. Chiron is a derivative of
vonNeumann Bernays G̈odel ( NBG ) set theory that is intended to be a
practical, generalpurpose logic for mechanizing mathematics. It
includes elements of type theory, a scheme for handling undefinedness,
and a facility for reasoning about the syntax of expressions. It is an
exceptionally wellsuited logic for formalizing biform theories. This
paper defines the notion of a biform theory, gives an overview of
Chiron, and illustrates how biform theories can be formalized in Chiron.",
paper = "Farm07.pdf",
keywords = "printed"
}\end{chunk}
\index{Carette, Jacques}
\index{Farmer, William M.}
\index{Sorge, Volker}
\begin{chunk}{ axiom.bib}
@inproceedings{Care07,
author = "Carette, Jacques and Farmer, William M. and Sorge, Volker",
title = {{A Rational Reconstruction of a System for Experimental
Mathematic s}},
booktitle = "14th Workshop on Automated Reasoning",
publisher = "unknown",
year = "2007",
abstract =
"In previous papers we described the implementation of a system
which combines mathematical object generation, transformation and
filtering, conjecture generation, proving and disproving for
mathematical discovery in nonassociative algebra. While the system
has generated novel, fully verified theorems, their construction
involved a lot of ad hoc communication between disparate systems. In
this paper we carefully reconstruct a specification of a subprocess
of the original system in a framework for trustable communication
between mathematics systems put forth by us. It employs the concept
of biform theories that enables the combined formalisation of the
axiomatic and algorithmic theories behind the generation
process. This allows us to gain a much better understanding of the
original system, and exposes clear generalisation opportunities.",
paper = "Care07.pdf",
keywords = "printed"
}\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@inproceedings{Farm00,
author = "Farmer, William M.",
title = {{A Proposal for the Development of an Interactive
Mathematic s Laboratory for Mathematics Eductions}},
booktitle = "Workshop on Deductions Systems for Mathematics Eduation",
pages = "2025",
year = "2000"
paper = "Farm00.pdf",
keywords = "axiomref, printed"
}\end{chunk}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@article{Farm04,
author = "Farmer, William M.",
title = {{MKM A New Interdisciplinary Field of Research}},
journal = "SIGSAM",
volume = "38",
pages = "4752",
year = "2004",
abstract =
"Mathematical Knowledge Management (MKM) is a new interdisciplinary
field of research in the intersection of mathematics, computer
science, library science, and scientific publishing. Its objective is
to develop new and better ways of managing mathematical knowledge
using sophisticated software tools. Its grand challenge is to create
a universal digital mathematics library (UDML), accessible via the
WorldWide Web, that contains essentially all mathematical knowledge
(intended for the public). The challenges facing MKM are daunting,
but a UDML, even just partially constructed, would transform how
mathematics is learned and practiced.",
paper = "Farm04.pdf",
keywords = "printed, axiomref"
}\end{chunk}
\index{Farmer, William M.}
\index{Mohrenschildt, Martin v.}
\begin{chunk}{ axiom.bib}
@inproceedings{Farm00a,
author = "Farmer, William M. and Mohrenschildt, Martin v.",
title = {{Transformers for Symbolic Computation and Formal Deduction}},
booktitle = "CADE17",
pages = "3645",
year = "2000",
abstract =
"A transformer is a function that maps expressions to expressions.
Many transformational operators — such as expression evaluators and
simplifiers, rewrite rules, rules of inference, and decision
procedures — can be represented by transformers. Computations and
deductions can be formed by applying sound transformers in
sequence. This paper introduces machinery for defining sound
transformers in the context of an axiomatic theory in a formal
logic. The paper is intended to be a first step in a development of an
integrated framework for symbolic computation and formal deduction.",
paper = "Farm00a.pdf",
keywords = "printed"
}\end{chunk}
\index{Farmer, William M.}
\index{Larjani, Pouya}
\begin{chunk}{ axiom.bib}
@misc{Farm14,
author = "Farmer, William M. and Larjani, Pouya",
title = {{Frameworks for Reasoning about Syntax that Utilize
Quotation and Evaluation}},
links = "\url{http://imps.mcmaster. }",ca/doc/ syntax. pdf
year = "2014",
abstract =
"It is often useful, if not necessary, to reason about the syntactic
structure of an expression in an interpreted language (i.e., a
language with a semantics). This paper introduces a mathematical
structure called a syntax framework that is intended to be an abstract
model of a system for reasoning about the syntax of an interpreted
language. Like many concrete systems for reasoning about syntax, a
syntax framework contains a mapping of expressions in the
interpreted language to syntactic values that represent the syntactic
structures of the expressions; a language for reasoning about the
syntactic values; a mechanism called quotation to refer to the
syntactic value of an expression; and a mechanism called evaluation to
refer to the value of the expression represented by a syntactic value.
A syntax framework provides a basis for integrating reasoning about
the syntax of the expressions with reasoning about what the
expressions mean. The notion of a syntax framework is used to discuss
how quotation and evaluation can be built into a language and to
define what quasiquotation is. Several examples of syntax frameworks
are presented.",
paper = "Farm14.pdf",
keywords = "printed"
}\end{chunk}
\index{Carette, Jacques}
\index{Farmer, William M.}
\index{O'Connor, Russell}
\begin{chunk}{ axiom.bib}
@misc{Care11c,
author = "Carette, Jacques and Farmer, William M. and O'Connor, Russell",
title = {{MathScheme: Project Description}},
year = "2011",
link = "\url{http://imps.mcmaster. }",ca/doc/ cicm2011 projdesc. pdf
paper = "Care11c.pdf",
keywords = "printed"
}\end{chunk}
\index{Carette, Jacques}
\index{Farmer, William M.}
\begin{chunk}{ axiom.bib}
@article{Care08,
author = "Carette, Jacques and Farmer, William M.",
title = {{HighLevel Theories}},
journal = "LNCS",
volume = "5144",
pages = "232245"
year = "2008",
abstract =
"We introduce highlevel theories in analogy with highlevel
programming languages. The basic point is that even though one can
define many theories via simple, lowlevel axiomatizations , that is
neither an effective nor a comfortable way to work with such theories.
We present an approach which is closer to what users of mathematics
employ, while still being based on formal structures.",
paper = "Care08.pdf",
keywords = "printed"
}\end{chunk}
\index{Carette, Jacques}
\index{O'Connor, Russell}
\begin{chunk}{ axiom.bib}
@article{Care12,
author = "Carette, Jacques and O'Connor, Russell",
title = {{Theory Presentation Combinators}},
journal = "LNCS",
volume = "7362",
year = "2012",
abstract =
"We motivate and give semantics to theory presentation combinators
as the foundational building blocks for a scalable library of
theories. The key observation is that the category of contexts and
fibered categories are the ideal theoretical tools for this
purpose.",
paper = "Care12.pdf",
keywords = "printed"
}\end{chunk}
\index{Musser, David R.}
\index{Kapur, Deepak}
\begin{chunk}{ axiom.bib}
@article{Muss82,
author = "Musser, David R. and Kapur, Deepak",
title = {{Rewrite Rule Theory and Abstract Data Type Analysis}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "7790",
year = "1982",
paper = "Muss82.pdf",
keywords = "axiomref"
}\end{chunk}
\index{Lazard, Daniel}
\begin{chunk}{ axiom.bib}
@article{Laza82,,
author = "Lazard, Daniel",
title = {{Commutative Algebra and Computer Algebra}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "4048",
year = "1982",
abstract =
"It is well known that computer algebra deals with commutative rings
such as the integers, the rationals, the modular integers and
polynomials over such rings.On the other hand, commutative algebra is that part of mathematics
which studies commutative rings.Our aim is to make this link more precise. It will appear that most of
the constructions which appear in classical commutative algebra can be
done explicitly in finite time. However, there are
exceptions. Moreover, most of the known algorithms are intractable :
The problems are generally exponential by themselves, but many
algorithms are overoverexponential. It needs a lot of work to find
better methods, and to implement them, with the final hope to open a
computation domain larger than this one which is possible by hand.To illustrate the limits and the possibilities of computerizing
commutative algebra, we describe an algorithm which tests the
primality of a polynomial ideal and we give an example of a single
algebraic extension of fields $K\subset L$ wuch that there exists an
algorithm of factorization for the polynomials over $k$, but not for
the polynomials over $L$.",
paper = "Laza82.pdf"
}\end{chunk}
\index{Hearn, Anthony C.}
\begin{chunk}{ axiom.bib}
@article{Hear82,,
author = "Hearn, Anthony C.",
title = {{REDUCE  A Case Study in Algebra System Development}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "263272",
year = "1982",
paper = "Hear82.pdf",
keywords = "axiomref"
}\end{chunk}
\index{Padget, J.A.}
\begin{chunk}{ axiom.bib}
@article{Padg82,
author = "Padget, J.A.",
title = {{Escaping from Intermediate Expression Swell: A Continuing Saga}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "256262",
year = "1982",
abstract =
"The notion of a closed continuation is introduced, is presented,
coroutines using function call and return based on this concept, are
applications and a functional dialect of LISP shown to be merely a
more general form of for coroutines in algebraic simplification and
are suggested, by extension function. expression Potential evaluation
and a specific example of their use is given in a novel attack on the
phenomenon of intermediate expression swell in polynomial
multiplication.",
paper = "Padg82.pdf"
}\end{chunk}
\index{Norman, Arthur}
\begin{chunk}{ axiom.bib}
@article{Norm82,
author = "Norman, Arthur",
title = {{The Development of a VectorBased Algebra System}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "237248",
year = "1982",
paper = "Norm82.pdf"
}\end{chunk}
\index{Bordoni, L.}
\index{Colagrossi, A.}
\index{Miola, A.}
\begin{chunk}{ axiom.bib}
@article{Bord82,
author = "Bordoni, L. and Colagrossi, A. and Miola, A.",
title = {{Linear Algebraic Approach for Computing Polynomial Resultant}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "231236",
year = "1982",
abstract =
"This paper presents a linear algebraic method for computing the
resultant of two polynomials. This method is based on the
computation of a determinant of order equal to the minimum of the
degrees of the two given polynomials. This method turns out to be
preferable to other known linear algebraic methods both from a
computational point of view and for a total generality respect to
the class of the given polynomials. Some relationships of this
method with the polynomial pseudoremainder operation are discussed.",
paper = "Bord82.pdf"
}\end{chunk}
\index{Arnon, Dennis S.}
\index{McCallum, Scott}
\begin{chunk}{ axiom.bib}
@article{Arno82a,
author = "Arnon, Dennis S. and McCallum, Scott",
title = {{Cylindrical Algebraic Decomposition by Quantifier Eliminations}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "215222",
year = "1982",
abstract =
"Cylindrical algebraic decompositions were introduced as a major
component of a new quantifier elimination algorithm for elementary
algebra and geometry (G. Collins, ~973). In the present paper we turn
the tables and show that one can use quantifier elimination for ele
mentary algebra and geometry to obtain a new version of the
cylindrical algebraic decomposi tion algorithm. A key part of our
result is a theorem, of interest in its own right, that relates the
multiplicities of the roots of a polynomial to their continuity.",
paper = "Arno82a.pdf"
}\end{chunk}
\index{Collins, George E.}
\begin{chunk}{ axiom.bib}
@article{Coll82a,
author = "Collins, George E.",
title = {{Factorization in Cylindrical Algebraic Decomposition  Abstract}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "212214",
year = "1982",
paper = "Coll82a.pdf"
}\end{chunk}
\index{Lazard, Daniel}
\begin{chunk}{ axiom.bib}
@article{Laza82a,
author = "Lazard, Daniel",
title = {{On Polynomial Factorization}},
journal = "Lecture Notes in Computer Science",
volume = "144",
pages = "144157",
year = "1982",
abstract =
"We present new algorithms for factoring univariate polynomials
over finite fields. They are variants of the algorithms of Camion
and CantorZassenhaus and differ from them essentially by
computing the primitive idempotents of the algebra $K[X]/f$ before
factoring $f$.These algorithms are probabilistic in the following sense. The
time of computation depends on random choices, but the validity of
the result does not depend on them. So, worst case complexity,
being infinite, is meaningless and we compute average
complexity. It appears that our and CantorZassenhaus algorithms
have the same asymptotic complexity and they are the best
algorithms actuall known; with elementary multiplication and GCD
computation, CantorZassenhaus algorithm is always bettern than
ours; with fast multiplication and GCD, it seems that ours is
better, but this fact is not yet proven.Finally, for factoring polynomials over the integers, it seems
that the best strategy consists in choosing prime moduli as big as
possible in the range where the time of the multiplication does
not depend on the size of the factors (machine word size). An
accurate computation of the involved constants would be needed for
proving this estimation.",
paper = "Laza82a.pdf"
}\end{chunk}
\index{Strachey, Christopher}
\index{Wadsworth, Christopher}
\begin{chunk}{ axiom.bib}
@article{Stra00a,
author = "Strachey, Christopher and Wadsworth, Christopher",
title = {{Continuations: A Mathematical Semantics for Handling Full Jumps}},
journal = "HigherOrder and Symbolic Computation",
volume = "13",
pages = "135152",
year = "2000",
abstract =
"This paper describes a method of giving the mathematical
semantics of programming languages which include the most general
form of jumps.",
paper = "Stra00a.pdf",
keywords = "printed"
}\end{chunk}
\index{Kaes, Stefan}
\begin{chunk}{ axiom.bib}
@article{Kaes88,
author = "Kaes, Stefan",
title = {{Parametric Overloading in Polymorphic Programming Languages}},
journal = "LNCS",
volume = "300",
pages = "131144",
year = "1988",
abstract =
"The introduction of unrestricted overloading in languagues with type
systems based on implicit parametric potymorphism generally destroys
the principal type property: namely that the type of every expression
can uniformly be represented by a single type expression over some set
of type variables. As a consequence, type inference in the presence
of unrestricted overloading can become a NPcomplete problem. In
this paper we define the concept of parametric overloading as a
restricted form of overloading which is easily combined with
parametric polymorphism. Parametric overloading preserves the
principal type property, thereby allowing the design of efficient type
inference algorithms. We present sound type deduction systems, both
for predefined and programmer defined overloading. Finally we state
that parametric overloading can be resolved either statically, at
compile time, or dynamically, during program execution.",
paper = "Kaes88.pdf",
keywords = "printed"
}\end{chunk}
\index{Kaes, Stefan}
\begin{chunk}{ axiom.bib}
@article{Kaes92,
author = "Kaes, Stefan",
title = {{Type Inference inthe Presence of Overloading, Subtyping and
Recursive Types}},
journal = "ACM Lisp Pointers",
volume = "5",
number = "1",
year = "1992",
pages = "193204",
abstract =
"We present a unified approach to type inference in the presence of
overloading and coercions based on the concept of {\sl constrained
types}. We define a generic inference system, show that subtyping and
overloading can be treated as a special instance of this system and
develop a simple algorithm to compute principal types. We prove the
decidability of type inference for hte class of {\sl decomposable
predicates} and deelop a canonical representation for principal types
based on {\sl most accurate simplifications} of constraint
sets. Finally, we investigate the extension of our techniques to
{\sl recursive types}.",
paper = "Kaes92.pdf",
keywords = "printed"
}\end{chunk}
\index{Hall, Cordelia V.}
\index{Hammond, Kevin}
\index{Jones, Simon L. Peyton}
\index{Wadler, Philip L.}
\begin{chunk}{ axiom.bib}
@article{Hall96,
author = "Hall, Cordelia V. and Hammond, Kevin and Jones, Simon L. Peyton
and Wadler, Philip L.",
title = {{Type Classes in Haskell}},
journal = "Trans. on Programming Langues and Systems",
volume = "18",
number = "2",
pages = "109138",
year = "1996",
abstract =
"This article de nes a set of type inference rules for resolving
overloading introduced by type classes, as used in the functional
programming language Haskell. Programs including type classes are
transformed into ones which may be typed by standard HindleyMilner
inference rules. In contrast to other work on type classes, the rules
presented here relate directly to Haskell programs. An innovative
aspect of this work is the use of secondorder lambda calculus to
record type information in the transformed program.",
paper = "Hall96.pdf",
keywords = "printed"
}\end{chunk}
\index{Dreyer, Derek}
\index{Harper, Robert}
\index{Chakravarty, Manuel M.T.}
\index{Keller, Gabriele}
\begin{chunk}{ axiom.bib}
@inproceedings{Drey07,
author = "Dreyer, Derek and Harper, Robert and Chakravarty, Manuel M.T.
and Keller, Gabriele",
title = {{Modlular Type Classes}},
booktitle = "Proc. POPL'07",
pages = "6370",
year = "2007",
abstract =
"ML modules and Haskell type classes have proven to be highly
effective tools for program structuring. Modules emphasize explicit
configuration of program components and the use of data abstraction.
Type classes emphasize implicit program construction and ad hoc
polymorphism. In this paper , we show how the implicitlytyped
style of type class programming may be supported within the framework
of an explicitlytyped module language by viewing type classes as a
particular mode of use of modules. This view offers a harmonious
integration of modules and type classes, where type class features,
such as class hierarchies and associated types, arise naturally as
uses of existing modulelanguage constructs, such as module
hierarchies and type components. In addition, programmers have
explicit control over which type class instances are available for
use by type inference in a given scope. We formalize our approach as
a HarperStonestyle elaboration relation, and provide a sound type
inference algorithm as a guide to implementation.",
paper = "Drey07.pdf",
keywords = "printed"
}\end{chunk}
\index{Wehr, Stefan}
\index{Chakravarty, Maneul M.T.}
\begin{chunk}{ axiom.bib}
@article{Wehr08,
author = "Wehr, Stefan and Chakravarty, Maneul M.T.",
title = {{ML Modules and Haskell Type Classes: A Constructive
Comparison }},
journal = "LNCS",
volume = "5356",
pages = "188204",
year = "2008",
abstract =
"Researchers repeatedly observed that the module system of ML and the
type class mechanism of Haskell are related. So far, this relationship
has received little formal investigation. The work at hand fills this
gap: It introduces typepreserving translations from modules to type
classes and vice versa, which enable a thorough comparison of the two
concepts.",
paper = "Wehr08.pdf",
keywords = "printed"
}\end{chunk}
\index{Stuckey, Peter J.}
\index{Sulzmann, Martin}
\begin{chunk}{ axiom.bib}
@article{Stuc05,
author = "Stuckey, Peter J. and Sulzmann, Martin",
title = {{A Theory of Overloading}},
journal = "ACM Trans. on Programming Languages and Systems",
volume = "27",
number = "6",
pages = "154",
year = "2005",
abstract =
"We present a novel approach to allow for overloading of
identifiers in the spirit of type classes. Our approach relies on
the combination of the HM(X) type system framework with Constraint
Handling Rules (CHRs). CHRs are a declarative language for writing
incremental constraint solvers, that provide our scheme with a
form of programmable type language. CHRs allow us to precisely
describe the relationships among overloaded identifiers. Under
some sufficient conditions on the CHRs we achieve decidable type
inference and the semantic meaning of programs is unambiguous. Our
approach provides a common formal basis for many type class
extensions such as multiparameter type classes and functional
dependencies.",
paper = "Stuc05.pdf",
keywords = "printed"
}\end{chunk}
\index{Reynolds, J.C.}
\begin{chunk}{ axiom.bib}
@article{Reyn85,
author = "Reynolds, J.C.",
title = {{Three Approaches to Type Structure}},
journal = "LNCS",
volume = "185",
year = "1985",
abstract =
"We examine three disparate views of the type structure of
programming languages: Milner's type deduction system and polymorphic
let construct, the theory of subtypes and generic operators, and
the polymorphic or secondorder typed lambda calculus. These
approaches are illustrated with a functional language including
product, sum and list constructors. The syntactic behavior of types
is formalized with type inference rules, bus their semantics is
treated intuitively.",
paper = "Reyn85.pdf",
keywords = "printed"
}\end{chunk}
\index{Balsters, Herman}
\index{Fokkinga, Maarten M.}
\begin{chunk}{ axiom.bib}
@article{Bals91,
author = "Balsters, Herman and Fokkinga, Maarten M.",
title = {{Subtyping can have a simple semantics}},
journal = "Theoretical Computer Science",
volume = "87",
pages = "8196",
year = "1991",
abstract =
"Consider a first order typed language, with semantics
$\llbracket~ \rrbracket$ for expressions and types. Adding
subtyping means that a partial order $\le$ on types is defined
and that the typing rules are extended to the effect that
expression $e$ has type $\tau$ whenever $e$ has type $\sigma$ and
$\sigma \le \tau$. We show how to adapt the semantics
$\llbracket~ \rrbracket$ in a {\sl simple set theoretic way},
obtaining a semantics $\llbracket~\rrbracket$ that satisfies, in
addition to some obvious requirements, also the property
$\llbracket\ sigma\rrbracket \subseteq $\llbracket\ tau\rrbracket$ ,
whenever $\sigma \le \tau$.",
paper = "Bals91.pdf",
keywords = "printed"
}\end{chunk}
\index{Cardelli, Luca}
\begin{chunk}{ axiom.bib}
@article{Card84,
author = "Cardelli, Luca",
title = {{A Semantics of Multiple Inheritance}},
journal = "LNCS",
volume = "173",
year = "1984",
paper = "Card84.pdf",
keywords = "printed"
}\end{chunk}
\index{Mosses, Peter}
\begin{chunk}{ axiom.bib}
@article{Moss84,
author = "Mosses, Peter",
title = {{A Basic Abstract Semantics Algebra}},
journal = "LNCS",
volume = "173",
year = "1984",
abstract =
"It seems that there are some pragmatic advantages in using Abstract
Semantic Algebras (ASAs) instead of Xnotation in denotational
semantics. The values of ASAs correspond to 'actions' (or
'processes'), and the operators correspond to primitive ways of
combining actions. There are simple ASAs for the various independent
'facets' of actions: a functional ASA for dataflow, an imperative ASA
for assignments, a declarative ASA for bindings, etc. The aim is to
obtain general ASAs by systematic combination of these simple ASAs.Here we specify a basic ASA that captures the common features of the
functional, imperative and declarative ASAs  and highlights their
differences. We discuss the correctness of ASA specifications, and
sketch the proof of the consistency and (limiting) completeness of the
functional ASA, relative to a simple model.Some familiarity with denotational semantics and algebraic
specifications is assumed.",
paper = "Moss84.pdf"
}\end{chunk}
\index{Gross, Jason}
\index{Chlipala, Adam}
\begin{chunk}{ axiom.bib}
@misc{Gros15,
author = "Gross, Jason and Chlipala, Adam",
title = {{Parsing Parses}},
link = "\url{https://people. }",csail.mit. edu/jgross/ personal website/ papers/ 2015parsing parsetrees. pdf
year = "2015",
abstract =
"We present a functional parser for arbitrary contextfree grammars,
together with soundness and completeness proofs, all inside Coq. By
exposing the parser in the right way with parametric polymorphism and
dependent types, we are able to use the parser to prove its own
soundness, and, with a little help from relational parametricity,
prove its own completeness, too. Of particular interest is one strange
instantiation of the type and value parameters: by parsing parse trees
instead of strings, we convince the parser to generate its own
completeness proof. We conclude with highlights of our experiences
iterating through several versions of the Coq development, and some
general lessons about dependently typed programming.",
paper = "Gros15.pdf",
keywords = "printed"
}\end{chunk}
\index{Wehr, Stefan}
\begin{chunk}{ axiom.bib}
@phdthesis{Wehr05,
author = "Wehr, Stefan",
title = {{ML Modules and Haskell Type Classes: A Constructive
Comparison }},
school = "Albert Ludwigs Universitat",
year = "2005",
abstract =
"Researchers repeatedly observed that the module system of ML and the
type class mechanism of Haskell are related. So far, this relationship
has received little formal investigation. The work at hand fills this
gap: It introduces typepreserving translations from modules to type
classes and vice versa, which enable a thorough comparison of the two
concepts.The source language of the first translation is a subset of
Standard ML. The target language is Haskell with common extensions
and one new feature, which was deeloped as part of this work. The
second translation maps a subset of Haskell 98 to ML, with
wellestablished extensions. I prove that the translations
preserve type correctness and provide implementations for both.Building on the insights obtained from the translations, I present
a thorough comparison between ML modules and Haskell type
classes. Moreover, I evaluate to what extent the techniques used
in the translations can be exploited for modular programming in
Haskell and for programming with adhoc polymorphism in ML.",
paper = "Wehr05.pdf"
}\end{chunk}
\index{Dreyer, Derek}
\index{Crary, Karl}
\index{Harper, Robert}
\begin{chunk}{ axiom.bib}
@article{Drey03,
author = "Dreyer, Derek and Crary, Karl and Harper, Robert",
title = {{A Type System for HigherOrder Modules}},
journal = "ACM SIGPLAN Notices",
volume = "38",
number = "1",
year = "2003",
link = "\url{https://www.cs. }",cmu.edu/ ~crary/ papers/ 2003/thoms/ thoms.pdf
abstract =
"We present a type theory for higherorder modules that accounts for
many central issues in module system design, including translucency,
applicativity , generativity , and modules as firstclass values.
Our type system harmonizes design elements from previous work,
resulting in a simple, economical account of modular programming. The
main unifying principle is the treatment of abstraction mechanisms
as computational effects. Our language is the first to provide a
complete and practical formalization of all of these critical issues
in module system design.",
paper = "Drey03.pdf",
keywords = "printed"
}\end{chunk}
\index{Crary, Karl}
\index{Harper, Robert}
\index{Puri, Sidd}
\begin{chunk}{ axiom.bib}
@inproceedings{Crar99,
author = "Crary, Karl and Harper, Robert and Puri, Sidd",
title = {{What is a Recursive Module}},
booktitle = "Conf. on Programming Language Design and Implementation",
year = "1999",
link = "\url{https://www.cs. }",cmu.edu/ ~crary/ papers/ 1999/recmod/ recmod. dvi
abstract =
"A hierarchical module system is an effective tool for structuring
large programs. Strictly hierarchical module systems impose an
acyclic ordering on import dependencies among program units. This
can impede modular programming by forcing mutuallydependent
components to be consolidated into a single module. Recently there
have been several proposals for module systems that admit cyclic
dependencies, but it is not clear how these proposals relate to
one another, nor how one mught integrate them into an expressive
module system such as that of ML.To address this question we provide a typetheoretic analysis of
the notion of a recursive module in the context of a
``phasedistinction' ' formalism for higherorder module
systems. We extend this calculus with a recursive module mechanism
and a new form of signature, called a {\sl recurslively dependent
signature}, to support the definition of recursive modules. These
extensions are justified by an interpretation in terms of more
primitive language constructs. This interpretation may also serve
as a guide for implementation.",
paper = "Crar99.pdf",
keywords = "printed"
}\end{chunk}
\index{Dreyer, Derek}
\index{Crary, Karl}
\index{Harper, Robert}
\begin{chunk}{ axiom.bib}
@techreport{Drey02,
author = "Dreyer, Derek and Crary, Karl and Harper, Robert",
title = {{A Type System for HigherOrder Modules (Expanded Version)}},
type = "technical report",
institution = "Carnegie Mellon University",
number = "CMUCS02122R",
year = "2002",
link = "\url{https://www.cs. }",cmu.edu/ ~crary/ papers/ 2003/thoms/ thomstr. pdf
abstract =
"We present a type theory for higherorder modules that accounts for
many central issues in module system design, including translucency,
applicativity , generativity , and modules as firstclass values.
Our type system harmonizes design elements from previous work,
resulting in a simple, economical account of modular programming. The
main unifying principle is the treatment of abstraction mechanisms
as computational effects. Our language is the first to provide a
complete and practical formalization of all of these critical issues
in module system design.",
paper = "Drey02.pdf"
}\end{chunk}
\index{Crary, Karl}
\begin{chunk}{ axiom.bib}
@techreport{Crar02,
author = "Crary, Karl",
title = {{Toward a Foundational Typed Assembly Language}},
institution = "Carnegie Mellon University",
number = "CMUCS02196",
year = "2002,
link = "\url{https://www.cs. }",cmu.edu/ ~crary/ papers/ 2003/talt/ talttr. pdf
abstract =
"We present the design of a typed assembly language called TALT that
supports heterogeneous tuples, disjoint sums, arrays, and a general
account of addressing modes. TALT also implements the von Neumann
model in which programs are stored in memory, and supports relative
addressing. Type safety for execution and for garbage collection are
shown by machinecheckable proofs. TALT is the first formalized typed
assembly language to provide any of these features.",
paper = "Crar02.pdf"
}\end{chunk}
\index{Mili, Ali}
\index{Aharon, Shir}
\index{Nadkarni, Chaitanya}
\begin{chunk}{ axiom.bib}
@article{Mili09,
author = "Mili, Ali and Aharon, Shir and Nadkarni, Chaitanya",
title = {{Mathematics for Reasoning about Loop Functions}},
journal = "Science of Computer Programming",
volume = "79",
year = "2009",
pages = "9891020",
abstract =
"The criticality of modern software applications, the pervasiveness of
malicious code concerns, the emergence of thirdparty software
development, and the preponderance of program inspection as a quality
assurance method all place a great premium on the ability to analyze
programs and derive their function in all circumstances of use and all
its functional detail. For Clike programming languages, one of the
most challenging tasks in this endeavor is the derivation of loop
functions. In this paper, we outline the premises of our approach to
this problem, present some mathematical results, and discuss how these
results can be used as a basis for building an automated tool that
derives the function of while loops under some conditions.",
paper = "Mili09.pdf",
keywords = "printed"
}\end{chunk}
\index{Piroi, Florina}
\index{Buchberger, Bruno}
\index{Rosenkranz, Camelia}
\begin{chunk}{ axiom.bib}
@misc{Piro08,
author = "Piroi, Florina and Buchberger, Bruno and Rosenkranz, Camelia",
title = {{Mathematical Journals as Reasoning Agents: Literature Review}},
year = "2008",
link = "\urlhttp://www.risc. jku.at/ publications/ download/ risc_3442/ MathAgents forSFB 200803 1012h00. pdf{}",
abstract =
"This report reviews the literature relevant for the research project
'Math−Agents: Mathematical Journals as Reasoning Agents' proposed by
Bruno Buchberger as a technology transfer project based on the results
of the SFB Project 'Scientific Computing', in particular the project
SFB 1302, 'Theorema'. The project aims at computer−supporting the
refereeing process of mathematical journals by tools that are mainly
based on automated reasoning and also at building up the knowledge
archived in mathematical journals in such a way that they can act as
interactive and active reasoning agents later on. In this report,
we review current mathematical software systems with a focus on the
availability of tools that can contribute to the goals of the Math−
Agents project.",
paper = "Piro08.pdf",
keywords = "printed"
}\end{chunk}
\index{Sokolowski, Stefan}
\begin{chunk}{ axiom.bib}
@article{Soko87,
author = "Sokolowski, Stefan",
title = {{Soundness of Hoare's Logic: An Automated Proof Using LCF}},
journal = "Trans. on Programming Languages and Systems",
volume = "9",
number = "1",
pages = "100120",
year = "1987",
abstract =
"This paper presents a natural deduction proof of Hoare's logic
carried out by the Edinburgh LCF theorem prover. The emphasis is
on the way Hoare's theory is presented to the LCF, which looks
very much like an exposition of syntax and semantics to human
readers; and on the programmable heuristics (tactics). We also
discuss some problems and possible improvements to the LCF.",
paper = "Soko87.pdf",
keywords = "printed"
}\end{chunk}
\index{Wadler, Philip}
\begin{chunk}{ axiom.bib}
@article{Wadl95,
author = "Wadler, Philip",
title = {{Monads for Functional Programming}},
journal = "LNCS",
volume = "925",
abstract =
"The use of monads to structure functional programs is
described. Monads provide a convenient framework for simulating
effects found in other languages, such as global state, exception
handling, output, or nondeterminism. Three case studies are
looked at in detail: how monads ease the modification of a simple
evaluator; how monads act as the basis of a datatype of arrays
subject to inplace update; and how monads can be used to build
parsers.",
paper = "Wadl95.pdf",
keywords = "printed"
}\end{chunk}
\index{Freeman, Tim}
\index{Pfenning, Frank}
\begin{chunk}{ axiom.bib}
@inproceedings{Free91,
author = "Freeman, Tim and Pfenning, Frank",
title = {{Refinement Types for ML}},
booktitle = "ACM SIGPLAN PLDI'91",
year = "1991",
link = "\url{http://www.cs. }",cmu.edu/ ~fp/papers/ pldi91. pdf
abstract =
"We describe a refinement of ML's type system allowing the
specification of recursively defined subtypes of userdefined
datatypes. The resulting system of {\sl refinement types}
preserves desirable properties of ML such as decidability of type
inference, while at the same time allowing more errors to be
detected at compiletime. The type system combines abstract
interpretation with ideas from the intersection type discipline,
but remains closely tied to ML in that refinement types are given
only to programs which are already welltyped in ML.",
paper = "Free91.pdf",
keywords = "printed"
}\end{chunk}
\index{Zeilberger, Noam}
\begin{chunk}{ axiom.bib}
@misc{Zeil16,
author = "Zeilberger, Noam",
title = {{Towards a Mathematical Science of Programming}},
year = "2016"
}\end{chunk}
\index{Zeilberger, Noam}
\begin{chunk}{ axiom.bib}
@inproceedings{Zeil16a,
author = "Zeilberger, Noam",
title = {{Principles of Type Refinement}},
booktitle = "OPLSS 2106",
link = "\url{http://noamz.org/ }",oplss16/ refinements notes.pdf
year = "2016",
paper = "Zeil16a.pdf"
}\end{chunk}
\index{McCarthy, John}
\begin{chunk}{ axiom.bib}
@incollection{Mcca63,
author = "McCarthy, John",
title = {{A Basis for a Mathematical Theory of Computation}},
booktitle = "Computer Programming and Formal Systems",
year = "1963",
paper = "Mcca63.pdf"
}\end{chunk}
\index{Scott, Dana S.}
\index{Strachey, Christopher}
\begin{chunk}{ axiom.bib}
@article{Scot71,
author = "Scott, Dana S. and Strachey, C.",
title = {{Towards a Mathematical Semantics for Computer Languages}},
journal = "Proc. Symp. on Computers and Automata",
volume = "21",
year = "1971",
abstract =
"Compilers for highlevel languages are generally constructed to
give a complete translation of the programs into machine
lanugage. As machines merely juggle bit patterns, the concepts of
the original language may be lost or at least obscured during this
passage. The purpose of a mathematical semantics is to give a
correct and meaningful correspondence between programs and
mathematical entities in a way that is entirely independent of an
implementation. This plan is illustrated in a very elementary
method with the usual idea of state transformations. The next
section shows why the mathematics of functions has to be modified
to accommodate recursive commands. Section 3 explains the
modification. Section 4 introduces the environments for handling
variables and identifiers and shows how the semantical equations
define equivalence of programs. Section 5 gives an exposition of
the new type of mathematical function spaces that are required for
the semantics of procedures when these are allowed in assignment
statements. The conclusion traces some of the background of the
project and points the way to future work.",
paper = "Scot71.pdf"
}\end{chunk}
\index{Mellies, PaulAndre}
\index{Zeilberger, Noam}
\begin{chunk}{ axiom.bib}
@inproceedings{Mell15,
author = "Mellies, PaulAndre and Zeilberger, Noam",
title = {{Functors are Type Refinement Systems}},
booktitle = "POPL'15",
publisher = "ACM",
year = "2015",
abstract =
"The standard reading of type theory through the lens of category
theory is based on the idea of viewing a type system as a category
of welltyped terms. We propose a basic revision of this reading;
rather than interpreting type systems as categories, we describe
them as {\sl functors} from a category of typing derivations to a
category of underlying terms. Then, turning this around, we
explain how in fact {\sl any} functor gives rise to a generalized
type system, with an abstract notion of type judgment, typing
derivations and typing rules. This leads to a purely categorical
reformulation of various natural classes of type systems as
natural classes of functors.The main purpose of this paper is to describe the general
framework (which can also be seen as providing a categorical
analysis of {\sl refinement types}, and to present a few
applications. As a larger case study, we revisit Reynold's paper
on ``The Meaning of Types'' (2000), showing how the paper's main
results may be reconstructed along these lines.",
paper = "Mell15.pdf",
keywords = "printed"
}\end{chunk}
\index{Shields, Mark}
\index{Jones, Simon Peyton}
\begin{chunk}{ axiom.bib}
@inproceedings{Shie02,
author = "Shields, Mark and Jones, Simon Peyton",
title = {{FirstClass Modules for Haskell}},
booktitle = "9th Int. Conf. on Foundations of ObjectOriented Languages",
pages = "2840",
year = "2002",
link = "\url{http://www.microsoft. }",com/en us/research/ wpcontent/ uploads/ 2016/02/ first_class_ modules. pdf
abstract =
"Though Haskell's module language is quite weak, its core language
is highly expressive. Indeed, it is tantalisingly close to being
able to express much of the structure traditionally delegated to a
separate module language. However, the encoding are awkward, and
some situations can't be encoded at all.In this paper we refine Haskell's core language to support
{\sl firstclass modules} with many of the features of MLstyle
modules. Our proposal cleanly encodes signatures, structures and
functors with the appropriate type abstraction and type sharing,
and supports recursive modules. All of these features work across
compilation units, and interact harmoniously with Haskell's class
system. Coupled with support for staged computation, we believe
our proposal would be an elegant approach to runtime dynamic
linking of structured code.Our work builds directly upon Jones' work on parameterised
signatures, Odersky and L\"aufer's system of higherranked type
annotations, Russo's semantics of ML modules using ordinary
existential and universal quantifications, and Odersky and
Zenger's work on nested types. We motivate the system by examples,
and include a more formal presentation in the appendix.",
paper = "Shie02.pdf",
keywords = "printed"
}\end{chunk}
\index{Dijkstra, E.W.}
\begin{chunk}{ axiom.bib}
@misc{Dijk71,
author = "Dijkstra, E.W.",
title = {{A Short Introduction to the Art of Programming}},
comment = "EWD316",
year = "1971",
paper = "Dijk71.pdf"
}\end{chunk}
\index{Steele, Guy Lewis}
\index{Sussman, Gerald Jay}
\begin{chunk}{ axiom.bib}
@techreport{Stee78a,
author = "Steele, Guy Lewis and Sussman, Gerald Jay",
title = {{The Art of the Interpreter or, The Modularity Complex (Parts
Zero, One, and Two}},
type = "technical report",
institution = "MIT AI Lab",
number = "AIM453",
year = "1978",
abstract =
"We examine the effects of various language design decisions on
the programming styles available to a user of the language, with
particular emphasis on the ability to incrementally construct
modular systems. At each step we exhibit an interactive
metacircular interpreter for the language under consideration.We explore the consequences of various variable binding
disciplines and the introduction of side effects. We find that
dynamic scoping is unsuitable for constructing procedural
abstractions, but has another role as an agent of modularity,
being a structured form of side effect. More general side effects
are also found to be necessary to promote modular style. We find
that the notion of side effect and the notion of equality (object
identity) are mutually constraining: to define one is to define
the other.The interpreters we exhibit are all written in a simple dialect of
LISP, and all implement LISPlike languages. A subset of these
interpreters constitute a partial historical reconstruction of the
actual evolution of LISP.",
paper = "Stee78a.pdf",
keywords = "printed"
}\end{chunk}
\index{Wadler, Philip}
\index{Findler, Robert Bruce}
\begin{chunk}{ axiom.bib}
@inproceedings{Wadl07a,
author = "Wadler, Philip and Findler, Robert Bruce",
title = {{WellTyped Programs Can't Be Blamed}},
booktitle = "Workshop on Scheme and Functional Programming",
year = "2007",,
pages = "1526",
abstract =
"We show how {\sl contracts} with blame fit naturally with recent
work on {\sl hybrid types} and {\sl gradual types}. Unlike hybrid
types or gradual types, we require casts in the source code, in
order to indicate where type errors may occur. Two (perhaps
surprising) aspects of our approach are that refined types can
provide useful static guarantees even in the absence of a theorem
prover, and that type {\sl dynamic} should not be regarded as a
supertype of all other types. We factor the wellknown notion of
subtyping into new notions of positive and negative subtyping, and
use these to characterise where positive and negative blame may
arise. Our approach sharpens and clarifies some recent results in
the literature.",
paper = "Wadl07a.pdf",
keywords = "printed"
}\end{chunk}
\index{Michaelson, Greg}
\begin{chunk}{ axiom.bib}
@book{Mich11,
author = "Michaelson, Greg",
title = {{Functional Programming Through Lambda Calculus}},
year = "2011",
publisher = "Dover",
isbn = "9780486478838"
}\end{chunk}
Branch metadata
 Branch format:
 Branch format 7
 Repository format:
 Bazaar repository format 2a (needs bzr 1.16 or later)