From d5ccd3b49dd5d92152c1b6f41b276d31e966dca0 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 27 Feb 2018 09:29:56 0500
Subject: [PATCH] books/bookvolbug bug 7335: type resolution failure
Goal: Axiom Maintenance

books/bookvolbug.pamphlet  15 +
changelog  2 +
patch  859 +
src/axiomwebsite/patches.html  2 +
4 files changed, 20 insertions(+), 858 deletions()
diff git a/books/bookvolbug.pamphlet b/books/bookvolbug.pamphlet
index 1365649..30369b5 100644
 a/books/bookvolbug.pamphlet
+++ b/books/bookvolbug.pamphlet
@@ 6,7 +6,7 @@
\chapter{Introduction}
\section{The Numbering Scheme}
\begin{verbatim}
bug 7335:
+bug 7336:
todo 342:
wish 1012:
meh 5:
@@ 18,6 +18,19 @@ nonextend 60077:
\end{verbatim}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{bug 7335: type resolution failure}
+\begin{verbatim}
+Infinite recursion in type checking. See resolveTTSpecial
+
+2^(1/2)/x/(%i)^(1/2)
+
+This happens during type resolution between
+Fraction(Polynomial(AlgebraicNumber)) and Expression(Complex(Integer))
+
+see https://groups.google.com/forum/#!topic/fricasdevel/czk7Ym_uWk
+\end{verbatim}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{bug 7334: coerce missing from EXPR(Quaternion (Complex (Float)))}
\begin{verbatim}
diff git a/changelog b/changelog
index 3bf0c88..e7f1f1a 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180227 tpd src/axiomwebsite/patches.html 20180227.02.tpd.patch
+20180227 tpd books/bookvolbug bug 7335: type resolution failure
20180227 tpd src/axiomwebsite/patches.html 20180227.01.tpd.patch
20180227 tpd books/bookvolbib add references
20180209 tpd src/axiomwebsite/patches.html 20180209.01.tpd.patch
diff git a/patch b/patch
index e2bf218..28a1aed 100644
 a/patch
+++ b/patch
@@ 1,858 +1,3 @@
books/bookvolbib add references

Goal: Proving Axiom Correct

\index{Gonzalez, Gabriel}
\begin{chunk}{axiom.bib}
@misc{Gonz18,
 author = "Gonzalez, Gabriel",
 title = {{How to Prove Large Software Projects Correct}},
 year = "2018",
 link = "\url{https://www.youtube.com/watch?v=moAfgDFVLUs}"
}

\end{chunk}

\index{Mietek, Bak}
\begin{chunk}{axiom.bib}
@misc{Miet15,
 author = "Mietek, Bak",
 title = {{Build Your Own Proof Assistant}},
 year = "2015",
 link = "\url{https://www.youtube.com/watch?v=7ujx1UyRmc}"
}

\end{chunk}

\index{Lepigre, Rodolphe}
\begin{chunk}{axiom.bib}
@phdthesis{Lepi16,
 author = "Lepigre, Rodolphe",
 title = {{Semantics and Implementation of an Extension of ML for
 Proving Programs}},
 year = "2016",
 school = "Universite Grenoble Alpes",
 link = "\url{http://lepigre.fr/these/manuscript_lepigre.pdf}",
 abstract =
 "In recent years, proof assistants have reached an impressive level
 of maturity. They have led to the certification of complex
 programs such as compilers and operating systems. Yet, using a
 proof assistant requires highly specialised skills and it remains
 very different from standard programming. To bridge this gap, we
 aim at designing an MLstyle programming language with support for
 proofs of programs, combining in a single tool the flexibility of
 ML and the fine specification features of a proof assistant. In
 other words, the system should be suitable both for programming
 (in the stronglytyped, functional sense) and for gradually
 increasing the level of guarantees met by programs, on a byneed
 basis.

 We thus define and study a callbyvalue language whose type
 system extends higherorder logic with an equality type over
 untyped programs, a dependent function type, classical logic and
 subtyping. The combination of callbyvalue evaluation, dependent
 functions and classical logic is known to raise consistency
 issues. To ensure the correctness of the system (logical
 consistency and runtime safety), we design a theoretical framework
 based on Krivine's classical realisability. The construction of
 the model relies on an essential property linking the different
 levels of interpretation of types in a novel way.

 We finally demonstrate the expressive power of our system using
 our prototype implementaiton, by proving properties of standard
 programs like the map function on lists or the insertion sort.",
 paper = "Lepi16.pdf"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Mapl18,
 author = "Maplesoft",
 title = {{Maple Computer Algebra Software}},
 year = "2018",
 link = "\url{https://www.maplesoft.com}"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Wolf18,
 author = "Wolfram, Stephen",
 title = {{Mathematica Website}},
 year = "2018",
 link = "\url{http://www.wolfram.com}"
}

\end{chunk}

\index{Harper, Robert}
\index{Mitchell, John C.}
\begin{chunk}{axiom.bib}
@inproceedings{Harp93a,
 author = "Harper, Robert and Mitchell, John C.",
 title = {{On the Type Structure of Standard ML}},
 booktitle = "Transactions on Programming Languages and Systems",
 publisher = "ACM",
 volume = "15",
 number = "2",
 pages = "211252",
 year = "1993",
 abstract =
 "Standard ML is a useful programming module facility. One notable
 feature of the core expression language of ML is that it is implictly
 typed: no explicit type information need be supplied by the
 programmer. In contrast, the module language of ML is explicitly
 typed; in particular, the types of parameters in parametric
 modules must be supplied by the programmer. We study the type
 structure of Standard ML by giving an explicitlytyped,
 polymmorphic function calculus that captures many of the essential
 aspects of both the core and module language. In this setting,
 implicitlytype core language expressions are reguarded as a
 convenient shorthand for an explicitlytyped counterpart in our
 function calculus. In contrast to the GirardReynolds polymorphic
 calculus, our function calculus is predicative: the type system
 may be built up by induction on type levels. We show that, in a
 precise sense, the language becomes inconsistent if restrictions
 imposed by type levels are relaxed. More specifically, we prove
 that the important programming features of ML cannot be added to
 any impredicative language, such as the GirardReynolds calcus,
 without implicitly assuming a type of all types.",
 paper = "Harp92a.pdf"
}

\end{chunk}

\index{Howard, W.H.}
\begin{chunk}{axiom.bib}
@misc{Howe69,
 author = "Howard, W.H.",
 title = {{The FormulaeasTypes Notion of Construction}},
 year = "1969",
 link = "\url{}",
 abstract =
 "The following consists of notes which were privately circulated in
 1969. Since they have been referred to a few times in the literature,
 it seems worth while to publish them. They have been rearranged for
 easier reading, and some inessential corrections have been made.

 The ultimate goal was to develop a notion of construction suitable for
 the interpretation of intuitionistic mathematics. The notion of
 construction developed in the notes is certainly too crude for that,
 so the use of the word construction is not very appropriate. However,
 the terminology has been kept in order to preserve the original title
 and also to preserve the character of the notes. The title has a
 second defect; namely, a type should be regarded as a abstract object
 whereas a formula is the name of a type.

 In Part I the ideas are illustrated for the intuitionistic
 propositional calculus and in Part II (page 6) they are applied to
 Heyting arithmetic.",
 paper = "Howe69.pdf"
}

\end{chunk}

\index{Meyer, Bertrand}
\begin{chunk}{axiom.bib}
@book{Meye92,
 author = "Meyer, Bertrand",
 title = {{Eiffel: The Language}},
 publisher = "Prentice Hall",
 year = "1992",
 isbn = "0132479257"
}

\end{chunk}

\index{Grogono, Peter}
\begin{chunk}{axiom.bib}
@misc{Grog91,
 author = "Grogono, Peter",
 title = {{Issues in the Design of an Object Oriented Programming
 Language}},
 link = "\url{http://users.encs.concordia.ca/~grogono/Writings/oopissue.pdf}",
 year = "1991",
 comment = "Published in Structured Programming",
 abstract =
 "The object oriented paradigm, which advocates bottomup program
 development, appears at first sight to run counter to the classical,
 topdown approach of structured programming. The deep requirement of
 structured programming, however, is that programming should be based
 on welldefined abstractions with clear meaning rather than on
 incidental characteris tics of computing machinery. This requirement
 can be met by object oriented programming and, in fact, object
 oriented programs may have better structure than programs obtained by
 functional decomposition.

 The definitions of the basic components of object oriented
 programming, object, class, and inheritance, are still sufficiently
 fluid to provide many choices for the designer of an object oriented
 language. Full support of objects in a typed language requires a
 number of features, including classes, inheritance, genericity,
 renaming, and redefinition. Although each of these features is simple
 in itself, interactions between features can become complex. For
 example, renaming and redefinition may interact in unexpected ways.
 In this paper, we show that appropriate design choices can yield a
 language that fulfills the promise of object oriented programming
 without sacrificing the requirements of structured programming.",
 paper = "Grog91.pdf"
}

\end{chunk}

\index{Mitchell, John}
\index{Meidal, Sigurd}
\index{Madhav, Neel}
\begin{chunk}{axiom.bib}
@inproceedings{Mitc91b,
 author = "Mitchell, John and Meidal, Sigurd and Madhav, Neel",
 title = {{An Extension of Standard ML Modules with Subtyping and
 Inheritance}},
 booktitle = "POPL'91",
 pages = "270278",
 year = "1991",
 isbn = "0897914198",
 abstract =
 "We describe a general module language integrating abstract data
 types, specifications and objectoriented concepts. The framework is
 based on the Standard ML module system, with three main extensions:
 subtyping, a form of object derived from ML structures, and inheritence
 primitives. The language aims at supporting a range of
 programming styles, including mixtures of objectoriented programming
 and programs built around specified algebraic or higherorder abstract
 data types. We separate specification from implementation,
 and provide independent inheritance mechanisms for each. In order to
 support binary operations on objects within this framework, we
 introduce ``internal interfaces// which govern the way that function
 components of one structure may access components of another. The
 language design has been tested by writing a number of program examples;
 an implementation is under development in the context of a
 larger project.",
 paper = "Mitc91b.pdf"
}

\end{chunk}

\index{Barton, John J.}
\index{Nackman, Lee R.}
\begin{chunk}{axiom.bib}
@book{Bart94,
 author = "Barton, John J. and Nackman, Lee R.",
 title = {{Scientific and Engineering C++}},
 publisher = "Pearson",
 year = "1994",
 isbn = "97800201533934"
}

\end{chunk}

\index{Ghelli, Giorgio}
\begin{chunk}{axiom.bib}
@article{Ghel91,
 author = "Ghelli, Giorgio",
 title = {{Modeling Features of ObjectOriented Languages in Second
 Order Functional Languages with Subtypes}},
 journal = "LNCS",
 volume = "489",
 pages = "311340",
 year = "1991",
 abstract =
 "Object oriented languages are an important tool to achieve software
 reusability in any kind of application and can increase dramatically
 software productivity in some special fields; they are also considered
 a logical step in the evolution of object oriented languages. But
 these languages lack a formal foundation, which is needed both to
 develop tools and as a basis for the future evolution of these
 languages; they lack also a strong type system, which would be
 essential to assure that level of reliability which is required to
 large evolving systems. Recently some researches have tried to
 insulate the basic mechanisms of object oriented languages and to
 embed them in strongly typed functional languages, giving to these
 mechanism a mathematical semantics and a set of strong type
 rules. This is a very promising approach which also allows a
 converging evolution of both the typed functional and the object
 oriented programming paradigms, making it possible a technology
 transfer in both directions. Most works in this field are very
 technical and deal just with one aspect of object oriented
 programming; many of them use a very similar framework. In this work
 we describe and exemplify that common framework and we survey some of
 the more recent and promising works on more specific features, using
 the framework introduced. We describe the resuks achieved and point
 out some problems which are still open, especially those arising from
 the interactions between different mechanisms.",
 paper = "Ghel91.pdf"
}

\end{chunk}

\index{Bruce, Kim}
\index{Mitchell, John C.}
\begin{chunk}{axiom.bib}
@inproceedings{Bruc92,
 author = "Bruce, Kim and Mitchell, John C.",
 title = {{PER Models of Subtyping, Recursive Types and HigherOrder
 Polymorphism}},
 booktitle = "POPL '92",
 pages = "316327",
 year = "1992",
 abstract =
 "We relate standard techniques for solving recursive domain equations
 to previous models with types interpreted as partial equivalence
 relations (per's) over a $D_\infty$ lambda model. This motivates a
 particular choice of type functions, which leads to an extension of
 such models to higherorder polymorphism. The resulting models provide
 natural interpretations for function spaces, records, recursively
 defined types, higherorder type functions, and bounded polymorphic
 types $\forall X <: Y.A$ where the bound may be of a higher kind. In
 particular, we may combine recursion and polymorphism in a way that
 allows the bound $Y$ in $\forall X <: Y.A$ to be recursively
 defined. The model may also be used to interpret socalled
 ``Fbounded polymorphism''. Together, these features allow us to
 represent several forms of type and type functions that seem to arise
 naturally in typed objectoriented programming.",
 paper = "Bruc92.pdf"
}

\end{chunk}

\index{Pierce, Benjamin C.}
\index{Turner, David N.}
\begin{chunk}{axiom.bib}
@inproceedings{Pier93,
 author = "Pierce, Benjamin C. and Turner, David N.",
 title = {{Objectoriented Programming without Recursive Types}},
 booktitle = "POPL'93",
 pages = "299312",
 year = "1993",
 abstract =
 "It is widely agreed that recursive types are inherent in the static
 typing of the essential mechanisms of objectoriented programming:
 encapsulation, message passing, subtyping, and inheritance. We
 demonstrate here that modeling object encapsulation in terms of
 existential types yields a substantially more straightforward
 explanation of these features in a simpler calculus without recursive
 types.",
 paper = "Pier93.pdf"
}

\end{chunk}

\index{Amadio, Roberto M.}
\index{Cardelli, Luca}
\begin{chunk}{axiom.bib}
@article{Amad93,
 author = "Amadio, Roberto M. and Cardelli, Luca",
 title = {{Subtyping Recursive Types}},
 journal = "TOPLAS '93",
 volume = "15",
 number = "4",
 year = "1993",
 pages = "575631",
 abstract =
 "We investigate the interactions of subtyping and recursive types, in
 a simply typed &lgr;calculus. The two fundamental questions here are
 whether two (recursive)types are in the subtype relation and whether a
 term has a type. To address the first question, we relate various
 definitions of type equivalence and subtyping that are induced by a
 model, an ordering on infinite trees, an algorithm, and a set of type
 rules. We show soundness and completeness among the rules, the
 algorithm, and the tree semantics. We also prove soundness and a
 restricted form of completeness for the model. To address the second
 question, we show that to every pair of types in the subtype relation
 we can associate a term whose denotation is the uniquely determined
 coercion map between the two types. Moreover, we derive an algorithm
 that, when given a term with implicit coercions, can infer its least
 type whenever possible.",
 paper = "Amad93.pdf"
}

\end{chunk}

\index{Cardelli, Luca}
\begin{chunk}{axiom.bib}
@inproceedings{Card88a,
 author = "Cardelli, Luca",
 title = {{Structural Subtyping and the Notion of Power Type}},
 booktitle = "POPL '88",
 year = "1988",
 publisher = "ACM",
 paper = "Card88a.pdf"
}

\end{chunk}

\index{Mitchell, John C.}
\begin{chunk}{axiom.bib}
@article{Mitc88a,
 author = "Mitchell, John C.",
 title = {{Polymorphic Type Inference and Containment}},
 journal = "Information and Computation",
 volume = "76",
 number = "23",
 year = "1988",
 pages = "211249",
 abstract =
 "Type expressions may be used to describe the functional behavior of
 untyped lambda terms. We present a general semantics of polymorphic
 type expressions over models of untyped lambda calculus and give
 complete rules for inferring types for terms. Some simplified typing
 theories are studied in more detail, and containments between types
 are investigated.",
 paper = "Mitch88a.pdf"
}

\end{chunk}

\index{Wirth, N.}
\begin{chunk}{axiom.bib}
@article{Wirt88,
 author = "Wirth, N.",
 title = {{Type Extensions}},
 journal = "TOPLAS",
 volume = "10",
 number = "2",
 year = "1988",
 pages = "203214",
 abstract =
 "Software systems represent a hierarchy of modules. Client modules
 contain sets of procedures that extend the capabilities of imported
 modules. This concept of extension is here applied to data
 types. Extended types are related to their ancestor in terms of a
 hierarchy. Variables of an extended type are compatible with variables
 of the ancestor type. This scheme is expressed by three language
 constructs only: the declaration of extended record types, the type
 test, and the type guard. The facility of extended types, which
 closely resembles the class concept, is defined in rigorous and
 concise terms, and an efficient implementation is presented.",
 paper = "Wirt88.pdf"
}

\end{chunk}

\index{Abadi, Martin}
\index{Cardelli, Luca}
\begin{chunk}{axiom.bib}
@inproceedings{Abad94,
 author = "Abadi, Martin and Cardelli, Luca",
 title = {{A Semantics of Object Types}},
 booktitle = "Symp. on Logic in Computer Science '94",
 publisher = "IEEE",
 year = "1994",
 abstract =
 "We give a semantics for a typed object calculus, an extension of
 System {\bf F} with object subsumption and method override. We interpret
 the calculus in a per model, proving the soundness of both typing and
 equational rules. This semantics suggests a syntactic translation
 from our calculus into a simpler calculus with neither subtyping nor
 objects",
 paper = "Abad94.pdf"
}

\end{chunk}

\index{Abadi, Martin}
\index{Cardelli, Luca}
\begin{chunk}{axiom.bib}
@inproceedings{Abad94a,
 author = "Abadi, Martin and Cardelli, Luca",
 title = {{A Theory of Primitive Objects: Untyped and FirstOrder Systems}},
 booktitle = "Proc. European Symposium on Programming",
 year = "1994",
 abstract =
 "We introduce simple object calculi that support method override and
 object subsumption. We give an untyped calculus, typing rules, and
 equational rules. We illustrate the expressiveness of our calculi and
 the pit falls that we avoid.",
 paper = "Abad94a.pdf"
}

\end{chunk}

\index{Lampson, B.}
\index{Burstall, R.}
\begin{chunk}{axiom.bib}
@article{Lamp88,
 author = "Lampson, B. and Burstall, R.",
 title = {{Pebble, a Kernel Language for Modules and Abstract Data Types}},
 journal = "Information and Computation",
 volume = "76",
 pages = "278346",
 year = "1988",
 abstract =
 "A small set of constructs can simulate a wide variety of apparently
 distinct features in modern programming languages. Using a kernel
 language called Pebble based on the typed lambda calculus with
 bindings, declarations, dependent types, and types as compile time
 values, we show how to build modules, interfaces and implementations,
 abstract data types, generic types, recursive types, and unions.
 Pebble has a concise operational semantics given by inference rules.",
 paper = "Lamp88.pdf"
}

\end{chunk}

\index{Ungar, David}
\index{Smith, Randall B.}
\begin{chunk}{axiom.bib}
@article{Unga91,
 author = "Ungar, David and Smith, Randall B.",
 title = {{SELF: The Power of Simplicity}},
 journal = "Lisp and Symbolic Computation",
 volume = "4",
 number = "3",
 year = "1991",
 publisher = "Kluwer",
 abstract =
 "SELF is an objectoriented language for exploratory programming
 based on a small number of simple and concrete ideas: prototypes,
 slots, and behavior. Prototypes combine inheritance and instantiation
 to provide a framework that is simpler and more flexible than most
 objectoriented languages. Slots unite variables and procedures into a
 single construct. This permits the inheritance hierarchy to take over
 the function of lexical scoping in conventional languages. Finally,
 because SELF does not distinguish state from behavior, it narrows the
 gaps between ordinary objects, procedures, and closures. SELF ’s
 simplicity and expressiveness offer new insights into objectoriented
 computation.",
 paper "Unga91.pdf"
}

\end{chunk}

\index{Herrlich, Horst}
\index{Strecker, G.E.}
\begin{chunk}{axiom.bib}
@book{Herr73,
 author = "Herrlich, Horst and Strecker, G.E.",
 title = {{Category Theory: An Introduction}},
 year = "1973",
 publisher = "Allyn and Bacon"
}

\end{chunk}

\index{Harper, Robert}
\index{Lillibridge, Mark}
\begin{chunk}{axiom.bib}
@inproceedings{Harp94,
 author = "Harper, Robert and Lillibridge, Mark",
 title = {{A TypeTheoretic Approach to HigherOrder Modules with Sharing}},
 booktitle = "POPL'21 Principles of Programming Languages",
 year = "1994",
 publisher = "ACM Press",
 abstract =
 "The design of a module system for constructing and maintaining
 large programs is a difficult task that raises a number of theoretical
 and practical issues. A fundamental issue is the management of the
 flow of information between program units at compile time via the
 notion of an interface. Experience has shown that fully opaque
 interfaces are awkward to use in practice since too much
 information is hidden, and that fully transparent interfaces lead to
 excessive interdependencies, creating problems for maintenance
 and separate compilation. The ``sharing'' specications of Standard ML
 address this issue by allowing the programmer to specify equational
 relationships between types in separate modules, but are not
 expressive enough to allow the programmer complete control over
 the propagation of type information between modules.

 These problems are addressed from a typetheoretic viewpoint by
 considering a calculus based on Girard's system $F_\omega$. The calculus
 differs from those considered in previous studies by relying exclusively
 on a new form of weak sum type to propagate information at
 compiletime, in contrast to approaches based on strong sums which
 rely on substitution. The new form of sum type allows for the
 specification of equational, as well as type and kind, information
 in interfaces. This provides complete control over the propagation
 of compiletime information between program units and is
 sufficient to encode in a straightforward way most uses of type
 sharing specifications in Standard ML. Modules are treated as
 ``firstclass'' citizens, and therefore the system supports
 higherorder modules and some objectoriented programming idioms: the
 language may be easily restricted to ``secondclass' modules found in
 MLlike languages.",
 paper = "Harp94.pdf"
}

\end{chunk}

\index{Wirth, N.}
\begin{chunk}{axiom.bib}
@misc{Wirt80,
 author = "Wirth, N.",
 title = {{Modula2}},
 year = "1980",
 link = "\url{http://www.adaauth.org/standards/12rm/RMFinal.pdf}",
 abstract =
 "Modula2 is a general purpose programming language primarily
 designed for system implementation. This report constitutes its
 definition in a concise, although informal style. It also
 describes the use of an implementation for the PDP11 computer.",
 paper = "Wirt80.pdf"
}

\end{chunk}

\index{Wirth, N.}
\begin{chunk}{axiom.bib}
@book{Wirt83,
 author = "Wirth, N.",
 title = {{Programming in Modula2}},
 publisher = "SpringerVerlag",
 year = "1983",
 isbn = "9783642968785"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@book{Adax12,
 author = "ISO/IEC 8652:2012(E)",
 title = {{Ada Reference Manual}},
 publisher = "U.S. Government",
 year = "2012",
 link = "\url{http://www.adaauth.org/standards/12rm/RMFinal.pdf}"
}

\end{chunk}

\index{MacQueen, David}
\begin{chunk}{axiom.bib}
@inproceedings{Macq86,
 author = "MacQueen, David",
 title = {{Using Dependent Types to Express Modular Structure}},
 booktitle = "Principles of Programming Languages POPL'13",
 publisher = "ACM Press",
 pages = "277286",
 year = "1986",
 link =
 "\url{https://people.mpisws.org/~dreyer/courses/modules/macqueen86.pdf}",
 paper = "Macq86.pdf"
}

\end{chunk}

\index{MacQueen, David}
\begin{chunk}{axiom.bib}
@inproceedings{Macq84,
 author = "MacQueen, David",
 title = {{Modules for Standard ML}},
 booktitle = "Conf. on Lisp and Functional Programming",
 publisher = "ACM Press",
 year = "1984",
 pages = "198207",
 abstract =
 "The functional programming language ML has been undergoing a thorough
 redesign during the past year, and the module facility described here
 has been proposed as part of the revised language, now called Standard
 ML. The design has three main goals: (1) to facilitate the structuring
 of large ML programs; (2) to support separate compilation and generic
 library units; and (3) to employ new ideas in the semantics of data
 types to extend the power of ML's polymorphic type system. It is based
 on concepts inherent in the structure of ML, primarily the notions of
 a declaration, its type signature, and the environment that it
 denotes.",
 paper = "Macq84.pdf"
}

\end{chunk}

\index{Harper, Robert}
\index{Mitchell, John C.}
\index{Moggi, Eugenio}
\begin{chunk}{axiom.bib}
@inproceedings{Harp89,
 author = "Harper, Robert and Mitchell, John C. and Moggi, Eugenio",
 title = {{HigherOrder Modules and the Phase Distinction}},
 booktitle = "Symp. on Principles of Programming Languages POPL'17",
 publisher = "ACM Press",
 year = "1989",
 comment = "CMUCS89198",
 link = "\url{https://www.cs.cmu.edu/~rwh/papers/phase/tr.pdf}",
 pages = "341354",
 abstract =
 "In earlier work, we used a typed function calculus, XML, with
 dependent types to analyze several aspects of the Standard ML type
 system. In this paper , we introduce a refinement of XML with a clear
 compiletime/runtime phase distinction, and a direct compiletime
 type checking algorithm. The calculus uses a finer separation of
 types into universes than XML and enforces the phase distinction using
 a nonstandard equational theory for module and signature
 expressions. While unusual from a typetheoretic point of view, the
 nonstandard equational theory arises naturally from the wellknown
 Grothendieck construction on an indexed category.",
 paper = "Harp89.pdf"
}

\end{chunk}

\index{Turner, Raymond}
\begin{chunk}{axiom.bib}
@book{Turn91,
 author = "Turner, Raymond",
 title = {{Constructive Foundations for Functional Languages}},
 publisher = "McGrawHill",
 year = "1991",
 isbn = "9780077074111"
}

\end{chunk}

\index{Zippel, Richard}
\begin{chunk}{axiom.bib}
@inproceedings{Zipp93,
 author = "Zippel, Richard",
 title = {{The Weyl Computer Algebra Substrate}},
 booktitle = "Design and Implementation of Symbolic Computation Systems '93",
 series = "DISCO 93",
 pages = "303=317",
 year = "1993",
 abstract =
 "Weyl is a new type of computer algebra substrate that extends an
 existing, object oriented programming language with symbolic computing
 mechanisms. Rather than layering a new language on top of an existing
 one, Weyl behaves like a powerful subroutine library, but takes heavy
 advantage of the ability to overload primitive arithmetic operations
 in the base language. In addition to the usual objects manipulated in
 computer algebra systems (polynomial, rational functions, matrices,
 etc.), domains (e.g., Z, Q[x, y, z]) are also first class objects in
 Weyl.",
 paper = "Zipp93.pdf",
 keywords = "axiomref"
}

\end{chunk}

\index{Leroy, Xavier}
\begin{chunk}{axiom.bib}
@inproceedings{Lero94,
 author = "Leroy, Xavier",
 title = {{Manifest Types, Modules, and Separate Compilation}},
 booktitle = "Principles of Programming Languages POPL'94",
 year = "1994",
 publisher = "ACM Press",
 pages = "109122",
 abstract =
 "This paper presents a variant of the SML module system
 that introduces a strict distinction between abstract types
 and manifest types (types whose definitions are part of the
 module specification), while retaining most of the expressive
 power of the SML module system. The resulting module
 system provides much better support for separate compilation.",
 paper = "Lero94.pdf"
}

\end{chunk}

\index{MacQueen, David}
\begin{chunk}{axiom.bib}
@inproceedings{Macq88,
 author = "MacQueen, David",
 title = {{An Implementation of Standard ML Modules}},
 booktitle = "Lisp and Functional Programming '88",
 year = "1988",
 pages = "212223",
 publisher = "ACM Press",
 abstract =
 "Standard ML includes a set of module constructs that support
 programming in the large. These constructs extend ML's basic
 polymorphic type system by introducing the dependent types of Martin
 L/Sf's Intuitionistic Type Theory. This paper discusses the problems
 involved in implementing Standard ML's modules and describes a
 practical, efficient solution to these problems. The representations
 and algorithms of this implementation were inspired by a detailed
 formal semantics of Standard ML developed by Milner, Tofte, and
 Harper. The implementation is part of a new Standard ML compiler that
 is written ia Standard ML using the module system.",
 paper = "Macq88.pdf"
}

\end{chunk}

\index{Cannon, John J.}
\index{Playoust, Catherine}
\begin{chunk}{axiom.bib}
@book{Cann01,
 author = "Cannon, John J. and Playoust, Catherine",
 title = {{An Introduction to Algebraic Programming with Magma}},
 year = "2001",
 publisher = "University of Sydney",
 paper = "Cann01.pdf"
}

\end{chunk}

\index{Nipkow, Tobias}
\index{Prehofer, Christian}
\begin{chunk}{axiom.bib}
@inproceedings{Nipk93,
 author = "Nipkow, Tobias and Prehofer, Christian",
 title = {{Type Checking Type Classes}},
 booktitle = "Principles of Programming Languages POPL'93",
 publisher = "ACM Press",
 year = "1993",
 pages = "409418"
 abstract =
 "We study the type inference problem for a system with type classes as
 in the functional programming language Haskell. Type classes are an
 extension of MLstyle polymorphism with overloading. We generalize
 Milner's work on polymorphism by introducing a separate context
 constraining the type variables in a typing judgement. This leads to
 simple type inference systems and algorithms which closely resemble
 those for ML. In particular we present a new unification algorithm
 which is an extension of syntactic unification with constraint
 solving. The existence of principal types follows from an analysis of
 this unification algorithm."
}

\end{chunk}

\index{Nipkow, Tobias}
\index{Prehofer, Christian}
\begin{chunk}{axiom.bib}
@article{Nipk95,
 author = "Nipkow, Tobias and Prehofer, Christian",
 title = {{Type Reconstruction for Type Classes}},
 journal = "J. of Functional Programming",
 year = "1995",
 pages = "201224",
 abstract =
 "We study the type inference problem for a system with type classes as
 in the functional programming language Haskell. Type classes are an
 extension of MLstyle polymorphism with overloading. We generalize
 Milner's work on polymorphism by introducing a separate context
 constraining the type variables in a typing judgement. This leads to
 simple type inference systems and algorithms which closely resemble
 those for ML. In particular we present a new unification algorithm
 which is an extension of syntactic unification with constraint
 solving. The existence of principal types follows from an analysis of
 this unification algorithm.",
 paper = "Nipk95.pdf"
}

\end{chunk}

\index{MacQueen, David}
\index{Tofte, Mads}
\begin{chunk}{axiom.bib}
@article{Macq94,
 author = "MacQueen, David and Tofte, Mads",
 title = {{A Semantics for Higherorder Functors}},
 journal = "LNCS",
 volume = "788",
 pages = "409423",
 year = "1994",
 abstract =
 "Standard ML has a module system that allows one to define parametric
 modules, called functors. Functors are ``firstorder,'' meaning
 that functors themselves cannot be passed as parameters or returned
 as results of functor applications. This paper presents a semantics
 for a higherorder module system which generalizes the module system
 of Standard ML. The higherorder functors described here are
 implemented in the current version of Standard ML of New Jersey and
 have proved useful in programming practice.",
 paper = "Macq94.pdf"
}

\end{chunk}
+books/bookvolbug bug 7335: type resolution failure
+Goal: Axiom Maintenance
\ No newline at end of file
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 48fc5b7..319b77f 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5910,6 +5910,8 @@ src/axiomwebsite/index.html updated per request
books/bookvolbib add references
20180227.01.tpd.patch
books/bookvolbib add references
+20180227.02.tpd.patch
+books/bookvolbug bug 7335: type resolution failure

1.9.1