From d4dcf932239b0e43492bcb72328709d91c85bc5f Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Sat, 6 Jan 2018 14:04:33 -0500
Subject: [PATCH] books/bookvolbib add references
Goal: Proving Axiom Correct
\index{Pierce, Benjamin C.}
\index{Turner, David N.}
\begin{chunk}{axiom.bib}
@techreport{Pier97,
author = "Pierce, Benjamin C. and Turner, David N.",
title = {{Local Type Inference}},
institution = "Indiana University",
year = "1997",
type = "CSCI Technical Report",
number = "493",
abstract =
"We study two partial type inference methods for a language combining
subtyping and impredicative polymorphism. Both methods are {\sl local}
in the sense that missing annotations are recovered using only
information from adjacent nodes in the syntax tree, without long
distance constraints such as unification variables. One method infers
type arguments in polymorphic applications using a local constraint
solver. The other infers annotations on bound variables in function
abstractions by propagating type constraints downward from enclosing
application nodes. We motivate our design choices by a statistical
analysis of the uses of type inference in a sizable body of existing
ML code.",
paper = "Pier97.pdf"
}
\end{chunk}
\index{Ruzicka, Peter}
\index{Privara, Igor}
\begin{chunk}{axiom.bib}
@article{Ruzi89,
author = "Ruzicka, Peter and Privara, Igor",
title = {{An Almost Linear Robinson Unification Algorithm}},
journal = "Acta Informatica",
volume = "27",
pages = "61-71",
year = "1989",
abstract =
"Further asymptotical improvement of original Robinson's unification
idea is presented. By postponing the so-called occur-check in Corbin
and Bidoit's quadratic rehabilitation of the Robinson algorithm at the
end of unification an almost linear unification algorithm is obtained.
In the worst case, the resulting algorithm has the time complexity
O(p.A(p)), where p is the size of input terms and A is the inverse to
the Ackermann function. Moreover, the practical experiments are
summarized comparing Corbin and Bidoit's quadratic algorithm with the
resulting almost linear unification algorithm based on Robinson's
principle. ",
paper = "Ruzi89.pdf"
}
\end{chunk}
\index{Robinson, J.A.}
\begin{chunk}{axiom.bib}
@article{Robi65,
author = "Robinson, J.A.",
title = {{A Machine-Oriented Logic Based on the Resolution Principle}},
journal = "ACM",
volume = "12",
pages = "23-41",
year = "1965",
abstract =
"Theorem-proving on the computer, using procedures based on the
fundamental theorem of Herbrand concerning the first-order predicate
calculus, is examined with a view towards improving the efficiency and
widening the range of practical applicability of these procedures. A
elose analysis of the process of substitution (of terms for
variables), and the process of truth-functional analysis of the
results of such substitutions, reveals that both processes can be
combined into a single new process (called resolution), iterating
which is vastty more effieient than the older cyclic procedures
consisting of substitution stages alternating with truth-functional
analysis stages.
The theory of the resolution process is presented in the form of a
system of first-order logic with .just one inference principle (the
resolution principle). The completeness of the system is proved; the
simplest proof-procedure based on the system is then the direct
implementation of the proof of completeness. Howewer, this procedure is
quite inefficient, and the paper concludes with a discussion of
several principles (called search principles) which are applicable to
the design of efficient proof-procedures employing resolution as the
basic logical process.",
paper = "Robi65.pdf"
}
\end{chunk}
\index{van Lamsweerde, Axel}
\begin{chunk}{axiom.bib}
@incollection{Lams00,
author = "van Lamsweerde, Axel",
title = {{Formal Specification: A Roadmap}},
booktitle = "The Future of Software Engineering",
publisher = "ACM Press",
year = "2000",
abstract =
"Formal specifications have been a focus of software engineering
research for many years and have been applied in a wide variety of
settings. Their industrial use is still limited but has been steadily
growing. After recalling the essence, role, usage, and pitfalls of
formal specification, the paper reviews the main specification
paradigms to date and discuss their evaluation criteria. It then
provides a brief assessment of the current strengths and weaknesses of
today's formal specification technology. This provides a basis for
formulating a number of requirements for formal specification to
become a core software engineering activity in the future.",
paper = "Lams00.pdf"
}
\end{chunk}
---
books/axiom.bib | 199 +++++++++++++++++++++++++++----------
books/bookvolbib.pamphlet | 217 +++++++++++++++++++++++++++++++----------
changelog | 2 +
patch | 116 +++++++++++++++++++++-
src/axiom-website/patches.html | 2 +
5 files changed, 430 insertions(+), 106 deletions(-)
diff --git a/books/axiom.bib b/books/axiom.bib
index fd9b710..3e85ba6 100644
--- a/books/axiom.bib
+++ b/books/axiom.bib
@@ -778,7 +778,7 @@ paper = "Brea89.pdf"
@article{Como91,
author = "Comon, Hubert and Lugiez, D. and Schnoebelen, Ph.",
- title = "A Rewrite-based Type Discipline for a Subset of Computer Algebra",
+ title = {{A Rewrite-based Type Discipline for a Subset of Computer Algebra}},
journal = "J. Symbolic Computation",
volume = "11",
number = "4",
@@ -801,7 +801,7 @@ paper = "Brea89.pdf"
@article{Cool92,
author = "Coolsaet, Kris",
- title = "A Quick Introduction to the Programming Language MIKE",
+ title = {{A Quick Introduction to the Programming Language MIKE}},
journal = "Sigplan Notices",
volume = "27",
number = "6",
@@ -819,7 +819,7 @@ paper = "Brea89.pdf"
@inproceedings{Dama82,
author = "Damas, Luis and Milner, Robin",
- title = "Principal Type-schemes for Functional Programs",
+ title = {{Principal Type-schemes for Functional Programs}},
booktitle = "POPL 82",
pages = "207-212",
year = "1982",
@@ -829,8 +829,8 @@ paper = "Brea89.pdf"
@book{Davi94,
author = "Davis, Martin D. and Sigal, Ron and Weyuker, Elaine J.",
- title = "Computability, Complexity, and Languages: Fundamentals of
- Theoretical Computer Science",
+ title = {{Computability, Complexity, and Languages: Fundamentals of
+ Theoretical Computer Science}},
publisher = "Academic Press",
year = "1994",
isbn = "978-0122063824"
@@ -838,7 +838,7 @@ paper = "Brea89.pdf"
@techreport{Ders89,
author = "Dershowitz, Nachum and Jouannaud, Jean-Pierre",
- title = "Rewrite Systems",
+ title = {{Rewrite Systems}},
year = "1989",
number = "478",
institution = "Laboratoire de Recherche en Informatique",
@@ -848,8 +848,8 @@ paper = "Brea89.pdf"
@book{Ehri85,
author = "Ehrig, Hartmut and Mahr, Bernd",
- title = "Fundamentals of Algebraic Specification 1: Equations and
- Initial Semantics",
+ title = {{Fundamentals of Algebraic Specification 1: Equations and
+ Initial Semantics}},
publisher = "Springer Verlag",
year = "1985",
isbn = "978-0387137186"
@@ -857,7 +857,7 @@ paper = "Brea89.pdf"
@inproceedings{Elli89,
author = "Elliott, Conal M.",
- title = "Higher-order Unification with Dependent Function Types",
+ title = {{Higher-order Unification with Dependent Function Types}},
booktitle = "Rewriting Techniques and Applications",
year = "1989",
pages = "121-136",
@@ -888,7 +888,7 @@ paper = "Brea89.pdf"
@article{Farm90,
author = "Farmer, William M.",
- title = "A Partial Functions Version of Church's Simple Theory of Types",
+ title = {{A Partial Functions Version of Church's Simple Theory of Types}},
journal = "The Journal of Symbolic Logic",
volume = "55",
number = "3",
@@ -941,7 +941,7 @@ paper = "Brea89.pdf"
@article{Faxe02,
author = "Faxen, Karl-Filip",
- title = "A Static Sematics for Haskell",
+ title = {{A Static Sematics for Haskell}},
year = "2002",
journal = "J. Functional Programming",
volume = "12",
@@ -969,14 +969,14 @@ paper = "Brea89.pdf"
@misc{Fija17,
author = "Fijalkow, Nathanael",
title =
- "Computing using the generators of a group: the Schreier-Sims' algorithm",
+ {{Computing using the generators of a group: the Schreier-Sims' algorithm}},
year = "2017",
link = "\url{https://www.cs.ox.ac.uk/blogs/nathanael-fijalkow/2016/01/27/computing-using-the-generators-of-a-group/}"
}
@phdthesis{Fode83,
author = "Foderaro, John K.",
- title = "The Design of a Language for Algebraic Computation Systems",
+ title = {{The Design of a Language for Algebraic Computation Systems}},
school = "U.C. Berkeley, EECS Dept.",
year = "1983",
link = "\url{http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-83-160.pdf}",
@@ -997,7 +997,7 @@ paper = "Brea89.pdf"
@inproceedings{Frue91,
author = "Fruehwirth, Thom and Shapiro, Ehud and Vardi, Moshe Y. and
Yardeni, Eyal",
- title = "Logic programs as types for logic programs",
+ title = {{Logic programs as types for logic programs}},
booktitle = "Proc. Sixth Annual IEEE Symp. on Logic in Comp. Sci.",
publisher = "IEEE",
pages = "300-309",
@@ -1024,7 +1024,7 @@ paper = "Brea89.pdf"
@article{Fuhx89,
author = "Fuh, You-Chin and Mishra, Prateek",
- title = "Polymorphic Subtype Inference -- Closing the Theory-Practice Gap",
+ title = {{Polymorphic Subtype Inference -- Closing the Theory-Practice Gap}},
journal = "Lecture Notes in Computer Science",
volume = "352",
year = "1989",
@@ -1034,7 +1034,7 @@ paper = "Brea89.pdf"
@article{Fuhx90,
author = "Fuh, You-Chin",
- title = "Type Inference with Subtypes",
+ title = {{Type Inference with Subtypes}},
journal = "Theoretical Computer Science",
volume = "73",
number = "2",
@@ -1061,7 +1061,7 @@ paper = "Brea89.pdf"
@misc{GAPx17,
author = "The GAP Group",
- title = "GAP - Reference Manual",
+ title = {{GAP - Reference Manual}},
year = "2017",
link = "\url{https://www.gap-system.org/Manuals/doc/ref/manual.pdf}"
}
@@ -1076,7 +1076,7 @@ paper = "Brea89.pdf"
@book{Gira89,
author = "Girard, Jean-Yves",
- title = "Proofs and Types",
+ title = {{Proofs and Types}},
publisher = "Cambridge University Press",
year = "1989"
}
@@ -1092,8 +1092,8 @@ paper = "Brea89.pdf"
@techreport{Gogu89,
author = "Goguen, Joseph and Meseguer, Jose",
- title = "Order-sorted Algebra I : Equational Deduction for Multiple
- Inheritance, Overloading, Exceptions, and Partial Operations",
+ title = {{Order-sorted Algebra I : Equational Deduction for Multiple
+ Inheritance, Overloading, Exceptions, and Partial Operations}},
type = "technical report",
institution = "SRI International",
year = "1989",
@@ -1102,8 +1102,8 @@ paper = "Brea89.pdf"
@article{Gogu92,
author = "Goguen, Joseph and Meseguer, Jose",
- title = "Order-sorted Algebra I : Equational Deduction for Multiple
- Inheritance, Overloading, Exceptions, and Partial Operations",
+ title = {{Order-sorted Algebra I : Equational Deduction for Multiple
+ Inheritance, Overloading, Exceptions, and Partial Operations}},
journal = "Theoretical Computer Science",
volume = "105",
number = "2",
@@ -1139,15 +1139,15 @@ paper = "Brea89.pdf"
@book{Gold83,
author = "Goldberg, Adele and Robson, David",
- title = "Smalltalk-80: The Language and Its Implementation",
+ title = {{Smalltalk-80: The Language and Its Implementation}},
publisher = "Addison-Wesley",
year = "1983"
}
@article{Goll90,
author = "Gollan, H. and Grabmeier, J.",
- title = "Algorithms in Representation Theory and their
- Realization in the Computer Algebra System Scratchpad",
+ title = {{Algorithms in Representation Theory and their
+ Realization in the Computer Algebra System Scratchpad}},
journal = "Bayreuther Mathematische Schriften",
volume = "33",
year = "1990",
@@ -1166,7 +1166,7 @@ paper = "Brea89.pdf"
@article{Gons71,
author = "Gonshor, H.",
- title = "Contributions to Genetic Algebras",
+ title = {{Contributions to Genetic Algebras}},
journal = "Proc. Edinburgh Mathmatical Society (Series 2)",
volume = "17",
number = "4",
@@ -1187,17 +1187,17 @@ paper = "Brea89.pdf"
@misc{Gowe17,
author = "Gowers, Timothy",
- title = "Group actions II: the orbit-stabilizer theorem",
+ title = {{Group actions II: the orbit-stabilizer theorem}},
year = "2017",
link = "\url{https://gowers.wordpress.com/2011/11/09/group-actions-ii-the-orbit-stabilizer-theorem/}"
}
@article{Grab87,
author = "Grabmeier, Johannes and Kerber, Adalbert",
- title = "The Evaluation of Irreducible Polynomial
+ title = {{The Evaluation of Irreducible Polynomial
Representations of the General Linear Groups
and of the Unitary Groups over Fields of
- Characteristic 0",
+ Characteristic 0}},
journal = "Acta Applicandae Mathematica",
volume = "8",
year = "1987",
@@ -1223,14 +1223,14 @@ paper = "Brea89.pdf"
@book{Grie78,
author = "Gries, David",
- title = "Programming Methodology",
+ title = {{Programming Methodology}},
publisher = "Springer-Verlag",
year = "1978"
}
@book{Grae79,
author = "Graetzer, George",
- title = "Universal Algebra",
+ title = {{Universal Algebra}},
publisher = "Springer",
isbn = "978-0-387-77486-2",
year = "1979",
@@ -1239,7 +1239,7 @@ paper = "Brea89.pdf"
@article{Harp93,
author = "Harper, Robert and Honsell, Furio and Plotkin, Gordon",
- title = "A Framework for Defining Logics",
+ title = {{A Framework for Defining Logics}},
journal = "J. ACM",
volume = "40",
number = "1",
@@ -1265,7 +1265,7 @@ paper = "Brea89.pdf"
@article{Hind69,
author = "Hindley, R.",
- title = "The Principal Type-Scheme of an Object in Combinatory Logic",
+ title = {{The Principal Type-Scheme of an Object in Combinatory Logic}},
journal = "Trans. AMS",
volume = "146",
year = "1969",
@@ -1275,7 +1275,7 @@ paper = "Brea89.pdf"
@article{Hodg95,
author = "Hodges, Wilfrid",
- title = "The Meaning of Specifications I: Domains and Initial Models",
+ title = {{The Meaning of Specifications I: Domains and Initial Models}},
journal = "Theoretical Computer Science",
volume = "192",
issue = "1",
@@ -1303,7 +1303,7 @@ paper = "Brea89.pdf"
@techreport{Howe87,
author = "Howe, Douglas J.",
- title = "The Computational Behaviour of Girard's Paradox",
+ title = {{The Computational Behaviour of Girard's Paradox}},
institution = "Cornell University",
year = "1987",
link = "\url{https://ecommons.cornell.edu/handle/1813/6660}",
@@ -1331,8 +1331,8 @@ paper = "Brea89.pdf"
Guzman, Maria M. and Hammond, Kevin and Hughes, John and
Johnsson, Thomas and Kieburtz, Dick and Nikhil, Rishiyur and
Patrain, Will and Peterson, John",
- title = "Report on the Programming Language Haskell, a non-strict
- functional language version 1.2",
+ title = {{Report on the Programming Language Haskell, a non-strict
+ functional language version 1.2}},
journal = "ACM SIGPLAN Notices",
volume = "27",
number = "5",
@@ -1350,7 +1350,7 @@ paper = "Brea89.pdf"
@misc{Huda99,
author = "Hudak, Paul and Peterson, John and Fasel, Joseph H.",
- title = "A Gentle Introduction to Haskell 98",
+ title = {{A Gentle Introduction to Haskell 98}},
year = "1999",
link = "\url{https://www.haskell.org/tutorial/haskell-98-tutorial.pdf}",
paper = "Huda99.pdf"
@@ -1358,7 +1358,7 @@ paper = "Brea89.pdf"
@book{Huet91,
author = "Huet, Gerard and Plotkin, G.",
- title = "Logical Frameworks",
+ title = {{Logical Frameworks}},
publisher = "Cambridge University",
year = "1991"
}
@@ -1372,7 +1372,7 @@ paper = "Brea89.pdf"
@article{Jame81,
author = "James, G. and Kerber, A.",
- title = "The Representation Theory of the Symmetric Group",
+ title = {{The Representation Theory of the Symmetric Group}},
journal = "Encycl. of Math. and its Appl.",
volume = "16",
algebra = "\newline\refto{package REP1 RepresentationPackage1}",
@@ -1382,7 +1382,7 @@ paper = "Brea89.pdf"
@book{Jone87,
author = "Jones, Simon Peyton",
- title = "The Implementation of Functional Programming Languages",
+ title = {{The Implementation of Functional Programming Languages}},
publisher = "Simon and Schuster",
year = "1987",
isbn = "0-13-453333-X",
@@ -1391,16 +1391,16 @@ paper = "Brea89.pdf"
@book{Joua90,
author = "Jouannaud, Jean-Pierre and Kirchner, Claude",
- title = "Solving Equations in Abstract Algebras: A Rule-based Survey of
- Unification",
+ title = {{Solving Equations in Abstract Algebras: A Rule-based Survey of
+ Unification}},
year = "1990",
publisher = "Universite do Paris-Sud"
}
@inproceedings{Joua91,
author = "Jouannaud, Jean Pierre and Okada, Mitsuhiro",
- title = "A Computation Model for Executable Higher-order Algebraic
- Specification Languages",
+ title = {{A Computation Model for Executable Higher-order Algebraic
+ Specification Languages}},
booktitle = "Symposium on Logic in Computer Science",
pages = "350-361",
isbn = "081862230X",
@@ -1428,8 +1428,8 @@ paper = "Brea89.pdf"
@article{Kaes92,
author = "Kaes, Stefan",
- title = "Type Inference in the Presence of Overloading, Subtyping, and
- Recursive Types",
+ title = {{Type Inference in the Presence of Overloading, Subtyping, and
+ Recursive Types}},
journal = "LISP Pointers",
volume = "V",
number = "1",
@@ -1440,7 +1440,7 @@ paper = "Brea89.pdf"
@incollection{Kalt83a,
author = "Kaltofen, E.",
- title = "Factorization of Polynomials",
+ title = {{Factorization of Polynomials}},
booktitle = "Computer Algebra - Symbolic and Algebraic Computation",
publisher = "ACM",
pages = "95-113",
@@ -1459,7 +1459,7 @@ paper = "Brea89.pdf"
@techreport{Kane90,
author = "Kanellakis, Paris C. and Mairson, Harry G. and Mitchell, John C.",
- title = "Unification and ML Type Reconstruction",
+ title = {{Unification and ML Type Reconstruction}},
link = "\url{ftp://ftp.cs.brown.edu/pub/techreports/90/cs90-26.pdf}",
institution = "Brown University",
year = "1990",
@@ -1486,7 +1486,7 @@ paper = "Brea89.pdf"
@inproceedings{Kfou88,
author = "Kfoury, A.J. and Tiuryn, J. and Utzyczyn, P.",
- title = "A Proper Extension of ML with an Effective Type-Assignment",
+ title = {{A Proper Extension of ML with an Effective Type-Assignment}},
booktitle = "POPL 88",
year = "1988",
pages = "58-69",
@@ -1504,7 +1504,7 @@ paper = "Brea89.pdf"
@article{Kfou93,
author = "Kfoury, A. J. and Tiuryn, J. and Urzyczyn, P.",
- title = "The Undecidability of the Semi-unification Problem",
+ title = {{The Undecidability of the Semi-unification Problem}},
journal = "Information and Computation",
volume = "102",
number = "1",
@@ -7373,6 +7373,26 @@ paper = "Brea89.pdf"
paper = "Hoar96.pdf"
}
+@incollection{Lams00,
+ author = "van Lamsweerde, Axel",
+ title = {{Formal Specification: A Roadmap}},
+ booktitle = "The Future of Software Engineering",
+ publisher = "ACM Press",
+ year = "2000",
+ abstract =
+ "Formal specifications have been a focus of software engineering
+ research for many years and have been applied in a wide variety of
+ settings. Their industrial use is still limited but has been steadily
+ growing. After recalling the essence, role, usage, and pitfalls of
+ formal specification, the paper reviews the main specification
+ paradigms to date and discuss their evaluation criteria. It then
+ provides a brief assessment of the current strengths and weaknesses of
+ today's formal specification technology. This provides a basis for
+ formulating a number of requirements for formal specification to
+ become a core software engineering activity in the future.",
+ paper = "Lams00.pdf"
+}
+
@article{Lind88,
author = "Lindsay, Peter A.",
title = {{A Survery of Mechanical Support for Formal Reasoning}},
@@ -7481,6 +7501,28 @@ paper = "Brea89.pdf"
paper = "Mart79.pdf"
}
+@techreport{Pier97,
+ author = "Pierce, Benjamin C. and Turner, David N.",
+ title = {{Local Type Inference}},
+ institution = "Indiana University",
+ year = "1997",
+ type = "CSCI Technical Report",
+ number = "493",
+ abstract =
+ "We study two partial type inference methods for a language combining
+ subtyping and impredicative polymorphism. Both methods are {\sl local}
+ in the sense that missing annotations are recovered using only
+ information from adjacent nodes in the syntax tree, without long
+ distance constraints such as unification variables. One method infers
+ type arguments in polymorphic applications using a local constraint
+ solver. The other infers annotations on bound variables in function
+ abstractions by propagating type constraints downward from enclosing
+ application nodes. We motivate our design choices by a statistical
+ analysis of the uses of type inference in a sizable body of existing
+ ML code.",
+ paper = "Pier97.pdf"
+}
+
@misc{Reid17,
author = "Reid, Alastair",
title = {{How can you trust formally varified software}},
@@ -7512,6 +7554,59 @@ paper = "Brea89.pdf"
isbn = "0-415-21534-X"
}
+@article{Robi65,
+ author = "Robinson, J.A.",
+ title = {{A Machine-Oriented Logic Based on the Resolution Principle}},
+ journal = "ACM",
+ volume = "12",
+ pages = "23-41",
+ year = "1965",
+ abstract =
+ "Theorem-proving on the computer, using procedures based on the
+ fundamental theorem of Herbrand concerning the first-order predicate
+ calculus, is examined with a view towards improving the efficiency and
+ widening the range of practical applicability of these procedures. A
+ elose analysis of the process of substitution (of terms for
+ variables), and the process of truth-functional analysis of the
+ results of such substitutions, reveals that both processes can be
+ combined into a single new process (called resolution), iterating
+ which is vastty more effieient than the older cyclic procedures
+ consisting of substitution stages alternating with truth-functional
+ analysis stages.
+
+ The theory of the resolution process is presented in the form of a
+ system of first-order logic with .just one inference principle (the
+ resolution principle). The completeness of the system is proved; the
+ simplest proof-procedure based on the system is then the direct
+ implementation of the proof of completeness. Howewer, this procedure is
+ quite inefficient, and the paper concludes with a discussion of
+ several principles (called search principles) which are applicable to
+ the design of efficient proof-procedures employing resolution as the
+ basic logical process.",
+ paper = "Robi65.pdf"
+}
+
+@article{Ruzi89,
+ author = "Ruzicka, Peter and Privara, Igor",
+ title = {{An Almost Linear Robinson Unification Algorithm}},
+ journal = "Acta Informatica",
+ volume = "27",
+ pages = "61-71",
+ year = "1989",
+ abstract =
+ "Further asymptotical improvement of original Robinson's unification
+ idea is presented. By postponing the so-called occur-check in Corbin
+ and Bidoit's quadratic rehabilitation of the Robinson algorithm at the
+ end of unification an almost linear unification algorithm is obtained.
+ In the worst case, the resulting algorithm has the time complexity
+ O(p.A(p)), where p is the size of input terms and A is the inverse to
+ the Ackermann function. Moreover, the practical experiments are
+ summarized comparing Corbin and Bidoit's quadratic algorithm with the
+ resulting almost linear unification algorithm based on Robinson's
+ principle. ",
+ paper = "Ruzi89.pdf"
+}
+
@article{Tryb92,
author = "Trybulec, Zinaida and Swieczkowska, Halina",
title = {{Some Remarks on The Language of Mathematical Texts}},
@@ -36309,7 +36404,7 @@ paper = "Brea89.pdf"
@misc{Pier17,
author = "Pierce, Benjamin",
- title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
+ title = {{DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)}},
year = "2017",
link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
}
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index ca94390..5391370 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -1253,7 +1253,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Como91,
author = "Comon, Hubert and Lugiez, D. and Schnoebelen, Ph.",
- title = "A Rewrite-based Type Discipline for a Subset of Computer Algebra",
+ title = {{A Rewrite-based Type Discipline for a Subset of Computer Algebra}},
journal = "J. Symbolic Computation",
volume = "11",
number = "4",
@@ -1280,7 +1280,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Cool92,
author = "Coolsaet, Kris",
- title = "A Quick Introduction to the Programming Language MIKE",
+ title = {{A Quick Introduction to the Programming Language MIKE}},
journal = "Sigplan Notices",
volume = "27",
number = "6",
@@ -1305,7 +1305,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@inproceedings{Dama82,
author = "Damas, Luis and Milner, Robin",
- title = "Principal Type-schemes for Functional Programs",
+ title = {{Principal Type-schemes for Functional Programs}},
booktitle = "POPL 82",
pages = "207-212",
year = "1982",
@@ -1321,8 +1321,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Davi94,
author = "Davis, Martin D. and Sigal, Ron and Weyuker, Elaine J.",
- title = "Computability, Complexity, and Languages: Fundamentals of
- Theoretical Computer Science",
+ title = {{Computability, Complexity, and Languages: Fundamentals of
+ Theoretical Computer Science}},
publisher = "Academic Press",
year = "1994",
isbn = "978-0122063824"
@@ -1335,7 +1335,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@techreport{Ders89,
author = "Dershowitz, Nachum and Jouannaud, Jean-Pierre",
- title = "Rewrite Systems",
+ title = {{Rewrite Systems}},
year = "1989",
number = "478",
institution = "Laboratoire de Recherche en Informatique",
@@ -1352,8 +1352,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Ehri85,
author = "Ehrig, Hartmut and Mahr, Bernd",
- title = "Fundamentals of Algebraic Specification 1: Equations and
- Initial Semantics",
+ title = {{Fundamentals of Algebraic Specification 1: Equations and
+ Initial Semantics}},
publisher = "Springer Verlag",
year = "1985",
isbn = "978-0387137186"
@@ -1365,7 +1365,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@inproceedings{Elli89,
author = "Elliott, Conal M.",
- title = "Higher-order Unification with Dependent Function Types",
+ title = {{Higher-order Unification with Dependent Function Types}},
booktitle = "Rewriting Techniques and Applications",
year = "1989",
pages = "121-136",
@@ -1403,7 +1403,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Farm90,
author = "Farmer, William M.",
- title = "A Partial Functions Version of Church's Simple Theory of Types",
+ title = {{A Partial Functions Version of Church's Simple Theory of Types}},
journal = "The Journal of Symbolic Logic",
volume = "55",
number = "3",
@@ -1472,7 +1472,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Faxe02,
author = "Faxen, Karl-Filip",
- title = "A Static Sematics for Haskell",
+ title = {{A Static Sematics for Haskell}},
year = "2002",
journal = "J. Functional Programming",
volume = "12",
@@ -1504,7 +1504,7 @@ paper = "Brea89.pdf"
@misc{Fija17,
author = "Fijalkow, Nathanael",
title =
- "Computing using the generators of a group: the Schreier-Sims' algorithm",
+ {{Computing using the generators of a group: the Schreier-Sims' algorithm}},
year = "2017",
link = "\url{https://www.cs.ox.ac.uk/blogs/nathanael-fijalkow/2016/01/27/computing-using-the-generators-of-a-group/}"
}
@@ -1515,7 +1515,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@phdthesis{Fode83,
author = "Foderaro, John K.",
- title = "The Design of a Language for Algebraic Computation Systems",
+ title = {{The Design of a Language for Algebraic Computation Systems}},
school = "U.C. Berkeley, EECS Dept.",
year = "1983",
link = "\url{http://digitalassets.lib.berkeley.edu/techreports/ucb/text/CSD-83-160.pdf}",
@@ -1543,7 +1543,7 @@ paper = "Brea89.pdf"
@inproceedings{Frue91,
author = "Fruehwirth, Thom and Shapiro, Ehud and Vardi, Moshe Y. and
Yardeni, Eyal",
- title = "Logic programs as types for logic programs",
+ title = {{Logic programs as types for logic programs}},
booktitle = "Proc. Sixth Annual IEEE Symp. on Logic in Comp. Sci.",
publisher = "IEEE",
pages = "300-309",
@@ -1575,7 +1575,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Fuhx89,
author = "Fuh, You-Chin and Mishra, Prateek",
- title = "Polymorphic Subtype Inference -- Closing the Theory-Practice Gap",
+ title = {{Polymorphic Subtype Inference -- Closing the Theory-Practice Gap}},
journal = "Lecture Notes in Computer Science",
volume = "352",
year = "1989",
@@ -1590,7 +1590,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Fuhx90,
author = "Fuh, You-Chin",
- title = "Type Inference with Subtypes",
+ title = {{Type Inference with Subtypes}},
journal = "Theoretical Computer Science",
volume = "73",
number = "2",
@@ -1622,7 +1622,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@misc{GAPx17,
author = "The GAP Group",
- title = "GAP - Reference Manual",
+ title = {{GAP - Reference Manual}},
year = "2017",
link = "\url{https://www.gap-system.org/Manuals/doc/ref/manual.pdf}"
}
@@ -1647,7 +1647,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Gira89,
author = "Girard, Jean-Yves",
- title = "Proofs and Types",
+ title = {{Proofs and Types}},
publisher = "Cambridge University Press",
year = "1989"
}
@@ -1672,8 +1672,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@techreport{Gogu89,
author = "Goguen, Joseph and Meseguer, Jose",
- title = "Order-sorted Algebra I : Equational Deduction for Multiple
- Inheritance, Overloading, Exceptions, and Partial Operations",
+ title = {{Order-sorted Algebra I : Equational Deduction for Multiple
+ Inheritance, Overloading, Exceptions, and Partial Operations}},
type = "technical report",
institution = "SRI International",
year = "1989",
@@ -1687,8 +1687,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Gogu92,
author = "Goguen, Joseph and Meseguer, Jose",
- title = "Order-sorted Algebra I : Equational Deduction for Multiple
- Inheritance, Overloading, Exceptions, and Partial Operations",
+ title = {{Order-sorted Algebra I : Equational Deduction for Multiple
+ Inheritance, Overloading, Exceptions, and Partial Operations}},
journal = "Theoretical Computer Science",
volume = "105",
number = "2",
@@ -1729,7 +1729,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Gold83,
author = "Goldberg, Adele and Robson, David",
- title = "Smalltalk-80: The Language and Its Implementation",
+ title = {{Smalltalk-80: The Language and Its Implementation}},
publisher = "Addison-Wesley",
year = "1983"
}
@@ -1741,8 +1741,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Goll90,
author = "Gollan, H. and Grabmeier, J.",
- title = "Algorithms in Representation Theory and their
- Realization in the Computer Algebra System Scratchpad",
+ title = {{Algorithms in Representation Theory and their
+ Realization in the Computer Algebra System Scratchpad}},
journal = "Bayreuther Mathematische Schriften",
volume = "33",
year = "1990",
@@ -1772,7 +1772,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Gons71,
author = "Gonshor, H.",
- title = "Contributions to Genetic Algebras",
+ title = {{Contributions to Genetic Algebras}},
journal = "Proc. Edinburgh Mathmatical Society (Series 2)",
volume = "17",
number = "4",
@@ -1797,7 +1797,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@misc{Gowe17,
author = "Gowers, Timothy",
- title = "Group actions II: the orbit-stabilizer theorem",
+ title = {{Group actions II: the orbit-stabilizer theorem}},
year = "2017",
link = "\url{https://gowers.wordpress.com/2011/11/09/group-actions-ii-the-orbit-stabilizer-theorem/}"
}
@@ -1809,10 +1809,10 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Grab87,
author = "Grabmeier, Johannes and Kerber, Adalbert",
- title = "The Evaluation of Irreducible Polynomial
+ title = {{The Evaluation of Irreducible Polynomial
Representations of the General Linear Groups
and of the Unitary Groups over Fields of
- Characteristic 0",
+ Characteristic 0}},
journal = "Acta Applicandae Mathematica",
volume = "8",
year = "1987",
@@ -1842,7 +1842,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Grie78,
author = "Gries, David",
- title = "Programming Methodology",
+ title = {{Programming Methodology}},
publisher = "Springer-Verlag",
year = "1978"
}
@@ -1853,7 +1853,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Grae79,
author = "Graetzer, George",
- title = "Universal Algebra",
+ title = {{Universal Algebra}},
publisher = "Springer",
isbn = "978-0-387-77486-2",
year = "1979",
@@ -1870,7 +1870,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Harp93,
author = "Harper, Robert and Honsell, Furio and Plotkin, Gordon",
- title = "A Framework for Defining Logics",
+ title = {{A Framework for Defining Logics}},
journal = "J. ACM",
volume = "40",
number = "1",
@@ -1900,7 +1900,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Hind69,
author = "Hindley, R.",
- title = "The Principal Type-Scheme of an Object in Combinatory Logic",
+ title = {{The Principal Type-Scheme of an Object in Combinatory Logic}},
journal = "Trans. AMS",
volume = "146",
year = "1969",
@@ -1914,7 +1914,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Hodg95,
author = "Hodges, Wilfrid",
- title = "The Meaning of Specifications I: Domains and Initial Models",
+ title = {{The Meaning of Specifications I: Domains and Initial Models}},
journal = "Theoretical Computer Science",
volume = "192",
issue = "1",
@@ -1946,7 +1946,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@techreport{Howe87,
author = "Howe, Douglas J.",
- title = "The Computational Behaviour of Girard's Paradox",
+ title = {{The Computational Behaviour of Girard's Paradox}},
institution = "Cornell University",
year = "1987",
link = "\url{https://ecommons.cornell.edu/handle/1813/6660}",
@@ -1991,8 +1991,8 @@ paper = "Brea89.pdf"
Guzman, Maria M. and Hammond, Kevin and Hughes, John and
Johnsson, Thomas and Kieburtz, Dick and Nikhil, Rishiyur and
Patrain, Will and Peterson, John",
- title = "Report on the Programming Language Haskell, a non-strict
- functional language version 1.2",
+ title = {{Report on the Programming Language Haskell, a non-strict
+ functional language version 1.2}},
journal = "ACM SIGPLAN Notices",
volume = "27",
number = "5",
@@ -2016,7 +2016,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@misc{Huda99,
author = "Hudak, Paul and Peterson, John and Fasel, Joseph H.",
- title = "A Gentle Introduction to Haskell 98",
+ title = {{A Gentle Introduction to Haskell 98}},
year = "1999",
link = "\url{https://www.haskell.org/tutorial/haskell-98-tutorial.pdf}",
paper = "Huda99.pdf"
@@ -2029,7 +2029,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Huet91,
author = "Huet, Gerard and Plotkin, G.",
- title = "Logical Frameworks",
+ title = {{Logical Frameworks}},
publisher = "Cambridge University",
year = "1991"
}
@@ -2055,7 +2055,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Jame81,
author = "James, G. and Kerber, A.",
- title = "The Representation Theory of the Symmetric Group",
+ title = {{The Representation Theory of the Symmetric Group}},
journal = "Encycl. of Math. and its Appl.",
volume = "16",
algebra = "\newline\refto{package REP1 RepresentationPackage1}",
@@ -2069,7 +2069,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Jone87,
author = "Jones, Simon Peyton",
- title = "The Implementation of Functional Programming Languages",
+ title = {{The Implementation of Functional Programming Languages}},
publisher = "Simon and Schuster",
year = "1987",
isbn = "0-13-453333-X",
@@ -2083,8 +2083,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@book{Joua90,
author = "Jouannaud, Jean-Pierre and Kirchner, Claude",
- title = "Solving Equations in Abstract Algebras: A Rule-based Survey of
- Unification",
+ title = {{Solving Equations in Abstract Algebras: A Rule-based Survey of
+ Unification}},
year = "1990",
publisher = "Universite do Paris-Sud"
}
@@ -2096,8 +2096,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@inproceedings{Joua91,
author = "Jouannaud, Jean Pierre and Okada, Mitsuhiro",
- title = "A Computation Model for Executable Higher-order Algebraic
- Specification Languages",
+ title = {{A Computation Model for Executable Higher-order Algebraic
+ Specification Languages}},
booktitle = "Symposium on Logic in Computer Science",
pages = "350-361",
isbn = "081862230X",
@@ -2131,8 +2131,8 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Kaes92,
author = "Kaes, Stefan",
- title = "Type Inference in the Presence of Overloading, Subtyping, and
- Recursive Types",
+ title = {{Type Inference in the Presence of Overloading, Subtyping, and
+ Recursive Types}},
journal = "LISP Pointers",
volume = "V",
number = "1",
@@ -2147,7 +2147,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@incollection{Kalt83a,
author = "Kaltofen, E.",
- title = "Factorization of Polynomials",
+ title = {{Factorization of Polynomials}},
booktitle = "Computer Algebra - Symbolic and Algebraic Computation",
publisher = "ACM",
pages = "95-113",
@@ -2172,7 +2172,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@techreport{Kane90,
author = "Kanellakis, Paris C. and Mairson, Harry G. and Mitchell, John C.",
- title = "Unification and ML Type Reconstruction",
+ title = {{Unification and ML Type Reconstruction}},
link = "\url{ftp://ftp.cs.brown.edu/pub/techreports/90/cs90-26.pdf}",
institution = "Brown University",
year = "1990",
@@ -2205,7 +2205,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@inproceedings{Kfou88,
author = "Kfoury, A.J. and Tiuryn, J. and Utzyczyn, P.",
- title = "A Proper Extension of ML with an Effective Type-Assignment",
+ title = {{A Proper Extension of ML with an Effective Type-Assignment}},
booktitle = "POPL 88",
year = "1988",
pages = "58-69",
@@ -2229,7 +2229,7 @@ paper = "Brea89.pdf"
\begin{chunk}{axiom.bib}
@article{Kfou93,
author = "Kfoury, A. J. and Tiuryn, J. and Urzyczyn, P.",
- title = "The Undecidability of the Semi-unification Problem",
+ title = {{The Undecidability of the Semi-unification Problem}},
journal = "Information and Computation",
volume = "102",
number = "1",
@@ -9956,6 +9956,30 @@ when shown in factored form.
\end{chunk}
+\index{van Lamsweerde, Axel}
+\begin{chunk}{axiom.bib}
+@incollection{Lams00,
+ author = "van Lamsweerde, Axel",
+ title = {{Formal Specification: A Roadmap}},
+ booktitle = "The Future of Software Engineering",
+ publisher = "ACM Press",
+ year = "2000",
+ abstract =
+ "Formal specifications have been a focus of software engineering
+ research for many years and have been applied in a wide variety of
+ settings. Their industrial use is still limited but has been steadily
+ growing. After recalling the essence, role, usage, and pitfalls of
+ formal specification, the paper reviews the main specification
+ paradigms to date and discuss their evaluation criteria. It then
+ provides a brief assessment of the current strengths and weaknesses of
+ today's formal specification technology. This provides a basis for
+ formulating a number of requirements for formal specification to
+ become a core software engineering activity in the future.",
+ paper = "Lams00.pdf"
+}
+
+\end{chunk}
+
\index{Lindsay, Peter A.}
\begin{chunk}{axiom.bib}
@article{Lind88,
@@ -10085,6 +10109,33 @@ when shown in factored form.
\end{chunk}
+\index{Pierce, Benjamin C.}
+\index{Turner, David N.}
+\begin{chunk}{axiom.bib}
+@techreport{Pier97,
+ author = "Pierce, Benjamin C. and Turner, David N.",
+ title = {{Local Type Inference}},
+ institution = "Indiana University",
+ year = "1997",
+ type = "CSCI Technical Report",
+ number = "493",
+ abstract =
+ "We study two partial type inference methods for a language combining
+ subtyping and impredicative polymorphism. Both methods are {\sl local}
+ in the sense that missing annotations are recovered using only
+ information from adjacent nodes in the syntax tree, without long
+ distance constraints such as unification variables. One method infers
+ type arguments in polymorphic applications using a local constraint
+ solver. The other infers annotations on bound variables in function
+ abstractions by propagating type constraints downward from enclosing
+ application nodes. We motivate our design choices by a statistical
+ analysis of the uses of type inference in a sizable body of existing
+ ML code.",
+ paper = "Pier97.pdf"
+}
+
+\end{chunk}
+
\index{Reid, Alastair}
\begin{chunk}{axiom.bib}
@misc{Reid17,
@@ -10124,6 +10175,68 @@ when shown in factored form.
\end{chunk}
+\index{Robinson, J.A.}
+\begin{chunk}{axiom.bib}
+@article{Robi65,
+ author = "Robinson, J.A.",
+ title = {{A Machine-Oriented Logic Based on the Resolution Principle}},
+ journal = "ACM",
+ volume = "12",
+ pages = "23-41",
+ year = "1965",
+ abstract =
+ "Theorem-proving on the computer, using procedures based on the
+ fundamental theorem of Herbrand concerning the first-order predicate
+ calculus, is examined with a view towards improving the efficiency and
+ widening the range of practical applicability of these procedures. A
+ elose analysis of the process of substitution (of terms for
+ variables), and the process of truth-functional analysis of the
+ results of such substitutions, reveals that both processes can be
+ combined into a single new process (called resolution), iterating
+ which is vastty more effieient than the older cyclic procedures
+ consisting of substitution stages alternating with truth-functional
+ analysis stages.
+
+ The theory of the resolution process is presented in the form of a
+ system of first-order logic with .just one inference principle (the
+ resolution principle). The completeness of the system is proved; the
+ simplest proof-procedure based on the system is then the direct
+ implementation of the proof of completeness. Howewer, this procedure is
+ quite inefficient, and the paper concludes with a discussion of
+ several principles (called search principles) which are applicable to
+ the design of efficient proof-procedures employing resolution as the
+ basic logical process.",
+ paper = "Robi65.pdf"
+}
+
+\end{chunk}
+
+\index{Ruzicka, Peter}
+\index{Privara, Igor}
+\begin{chunk}{axiom.bib}
+@article{Ruzi89,
+ author = "Ruzicka, Peter and Privara, Igor",
+ title = {{An Almost Linear Robinson Unification Algorithm}},
+ journal = "Acta Informatica",
+ volume = "27",
+ pages = "61-71",
+ year = "1989",
+ abstract =
+ "Further asymptotical improvement of original Robinson's unification
+ idea is presented. By postponing the so-called occur-check in Corbin
+ and Bidoit's quadratic rehabilitation of the Robinson algorithm at the
+ end of unification an almost linear unification algorithm is obtained.
+ In the worst case, the resulting algorithm has the time complexity
+ O(p.A(p)), where p is the size of input terms and A is the inverse to
+ the Ackermann function. Moreover, the practical experiments are
+ summarized comparing Corbin and Bidoit's quadratic algorithm with the
+ resulting almost linear unification algorithm based on Robinson's
+ principle. ",
+ paper = "Ruzi89.pdf"
+}
+
+\end{chunk}
+
\index{Trybulec, Zinaida}
\index{Swieczkowska, Halina}
\begin{chunk}{axiom.bib}
@@ -54231,7 +54344,7 @@ Springer-Verlag, Heidelberg, 1982, ISBN 0-387-90693-2
\begin{chunk}{axiom.bib}
@misc{Pier17,
author = "Pierce, Benjamin",
- title = "DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)",
+ title = {{DeepSpec Summer School, Coq Intensive, Part 1 (July 13,2017)}},
year = "2017",
link = "\url{https://www.youtube.com/watch?v=jG61w5pOc2A}"
}
diff --git a/changelog b/changelog
index 6e92fc1..4bbbedc 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20180106 tpd src/axiom-website/patches.html 20180106.01.tpd.patch
+20180106 tpd books/bookvolbib add references
20180101 tpd src/axiom-website/patches.html 20180101.02.tpd.patch
20180101 tpd src/axiom-website/documentation.html add Pierce quote about TeX
20180101 tpd src/axiom-website/patches.html 20180101.01.tpd.patch
diff --git a/patch b/patch
index 43ce9d3..88fc941 100644
--- a/patch
+++ b/patch
@@ -1,4 +1,116 @@
-src/axiom-website/documentation.html add Pierce quote about TeX
+books/bookvolbib add references
-Goal: Maintenance
+Goal: Proving Axiom Correct
+\index{Pierce, Benjamin C.}
+\index{Turner, David N.}
+\begin{chunk}{axiom.bib}
+@techreport{Pier97,
+ author = "Pierce, Benjamin C. and Turner, David N.",
+ title = {{Local Type Inference}},
+ institution = "Indiana University",
+ year = "1997",
+ type = "CSCI Technical Report",
+ number = "493",
+ abstract =
+ "We study two partial type inference methods for a language combining
+ subtyping and impredicative polymorphism. Both methods are {\sl local}
+ in the sense that missing annotations are recovered using only
+ information from adjacent nodes in the syntax tree, without long
+ distance constraints such as unification variables. One method infers
+ type arguments in polymorphic applications using a local constraint
+ solver. The other infers annotations on bound variables in function
+ abstractions by propagating type constraints downward from enclosing
+ application nodes. We motivate our design choices by a statistical
+ analysis of the uses of type inference in a sizable body of existing
+ ML code.",
+ paper = "Pier97.pdf"
+}
+
+\end{chunk}
+
+\index{Ruzicka, Peter}
+\index{Privara, Igor}
+\begin{chunk}{axiom.bib}
+@article{Ruzi89,
+ author = "Ruzicka, Peter and Privara, Igor",
+ title = {{An Almost Linear Robinson Unification Algorithm}},
+ journal = "Acta Informatica",
+ volume = "27",
+ pages = "61-71",
+ year = "1989",
+ abstract =
+ "Further asymptotical improvement of original Robinson's unification
+ idea is presented. By postponing the so-called occur-check in Corbin
+ and Bidoit's quadratic rehabilitation of the Robinson algorithm at the
+ end of unification an almost linear unification algorithm is obtained.
+ In the worst case, the resulting algorithm has the time complexity
+ O(p.A(p)), where p is the size of input terms and A is the inverse to
+ the Ackermann function. Moreover, the practical experiments are
+ summarized comparing Corbin and Bidoit's quadratic algorithm with the
+ resulting almost linear unification algorithm based on Robinson's
+ principle. ",
+ paper = "Ruzi89.pdf"
+}
+
+\end{chunk}
+
+\index{Robinson, J.A.}
+\begin{chunk}{axiom.bib}
+@article{Robi65,
+ author = "Robinson, J.A.",
+ title = {{A Machine-Oriented Logic Based on the Resolution Principle}},
+ journal = "ACM",
+ volume = "12",
+ pages = "23-41",
+ year = "1965",
+ abstract =
+ "Theorem-proving on the computer, using procedures based on the
+ fundamental theorem of Herbrand concerning the first-order predicate
+ calculus, is examined with a view towards improving the efficiency and
+ widening the range of practical applicability of these procedures. A
+ elose analysis of the process of substitution (of terms for
+ variables), and the process of truth-functional analysis of the
+ results of such substitutions, reveals that both processes can be
+ combined into a single new process (called resolution), iterating
+ which is vastty more effieient than the older cyclic procedures
+ consisting of substitution stages alternating with truth-functional
+ analysis stages.
+
+ The theory of the resolution process is presented in the form of a
+ system of first-order logic with .just one inference principle (the
+ resolution principle). The completeness of the system is proved; the
+ simplest proof-procedure based on the system is then the direct
+ implementation of the proof of completeness. Howewer, this procedure is
+ quite inefficient, and the paper concludes with a discussion of
+ several principles (called search principles) which are applicable to
+ the design of efficient proof-procedures employing resolution as the
+ basic logical process.",
+ paper = "Robi65.pdf"
+}
+
+\end{chunk}
+
+\index{van Lamsweerde, Axel}
+\begin{chunk}{axiom.bib}
+@incollection{Lams00,
+ author = "van Lamsweerde, Axel",
+ title = {{Formal Specification: A Roadmap}},
+ booktitle = "The Future of Software Engineering",
+ publisher = "ACM Press",
+ year = "2000",
+ abstract =
+ "Formal specifications have been a focus of software engineering
+ research for many years and have been applied in a wide variety of
+ settings. Their industrial use is still limited but has been steadily
+ growing. After recalling the essence, role, usage, and pitfalls of
+ formal specification, the paper reviews the main specification
+ paradigms to date and discuss their evaluation criteria. It then
+ provides a brief assessment of the current strengths and weaknesses of
+ today's formal specification technology. This provides a basis for
+ formulating a number of requirements for formal specification to
+ become a core software engineering activity in the future.",
+ paper = "Lams00.pdf"
+}
+
+\end{chunk}
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 64de0b3..2eb0f34 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5886,6 +5886,8 @@ src/axiom-website/index.html update goal list

books/bookheader.tex add date and git master

20170101.02.tpd.patch
src/axiom-website/documentation.html add Pierce quote about TeX

+20180106.01.tpd.patch
+books/bookvolbib add references

--
1.9.1