From b7fe8923afab40710a1377efe423203bcdb3022a Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 20 Feb 2017 18:33:03 -0500
Subject: [PATCH] books/bookvolbib add additional references
Goal: Proving Axiom Correct
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@inproceedings{Dybj90,
author = "Dybjer, Peter",
title = {Inductive Sets and Families in Marin-L\"of's Type Theory and
Their Set-Theoretic Semantics},
booktitle = "Proc. First Workshop on Logical Frameworks",
year = "1990",
link =
"\url{http://www.cse.chalmers.se/~peterd/papers/Setsem\_Inductive.pdf}",
abstract =
"{Martin-L\"of}'s type theory is presented in several steps. The kernel
is a dependently typed $\lambda$-calculs. Then there are schemata for
inductive sets and families of sets and for primitive recursive functions
and families of functions. Finally, there are set formers (generic
polymorphism) and universes. At each step syntax, inference rules, and
set-theoretic sematics are given",
paper = "Dybj90.pdf"
}
\end{chunk}
\index{Goguen, Healfdene}
\index{McBride, Conor}
\index{McKinna, James}
\begin{chunk}{axiom.bib}
@article{Gogu06,
author = "Goguen, Healfdene and McBride, Conor and McKinna, James",
title = "Eliminating Dependent Pattern Matching",
year = "2006",
journal = "Lecture Notes in Computer Science",
volume = "4060",
pages = "521-540",
link = "\url{http://cs.ru.nl/~james/RESEARCH/goguen2006.pdf}",
abstract =
"This paper gives a reduction-preserving translation from Coquand's
{\sl dependent pattern matching} into a traditional type theory
with universes, inductive types and relations and the axiom K. This
translation serves as a proof of termination for structurally
recursive pattern matching programs, provides an implementable
compilation technique in the style of functional programming languages,
and demonstrates the equivelence with a more easily understood type
theory.",
paper = "Gogu06.pdf"
}
\end{chunk}
\index{McBride, Conor}
\index{Goguen, Healfdene}
\index{McKinna, James}
\begin{chunk}{axiom.bib}
@article{Mcbr06,
author = "McBride, Conor and Goguen, Healfdene and McKinna, James",
title = "A Few Constructions on Constructors",
journal = "Lecture Notes in Computer Science",
volume = "3839",
pages = "186-200",
year = "2006",
link = "\url{http://www.strictlypositive.org/concon.ps.gz}",
abstract =
"We present four constructions for standard equipment which can be
generated for every inductive datatype: case analysis, structural
recursion, no confusion, acyclicity. Our constructions follow a
two-level approach -- they require less work than the standard
techniques which inspired them. Moreover, given a suitably
heterogeneous notion of equality, they extend without difficulty to
inductive families of datatypes. These constructions are vital
components of the translation from dependently typed programs in
pattern matching style to the equivalent programs expressed in terms
of induction principles and as such play a crucial behind-the-scenes
role in Epigram.",
paper = "Mcbr06.pdf"
}
\end{chunk}
\index{Bove, Ana}
\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
@misc{Bove08,
author = "Bove, Ana and Dybjer, Peter",
title = "Dependent Types at Work",
year = "2008",
comment = "Lecture notes from LerNET Summer School, Piriapolis",
link =
"\url{http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf}",
abstract =
"In these lecture notes we give an introduction to functional
programming with dependent types. We use the dependently typed
programming language Agda which is an extension of {Martin-L\"of} type
theory. First we show how to do simply typed functional programming in
the style of Haskell and ML. Some differences between Agda's type
system and the Hindley-Milner type system of Haskell and ML are also
discussed. Then we show how to use dependent types for programming and
we explain the basic ideas behind type-checking dependent types. We go
on to explain the Curry-Howard identification of propositions and
types. This is what makes Agda a programming logic and not only a
programming language. According to Curry-Howard, we identify programs
and proofs, something which is possible only by requiring that all
programs terminate. However, at the end of these notes we present a
method for encoding partial and general recursive functions as total
functions using dependent types.",
paper = "Bove08.pdf"
}
\end{chunk}
\index{Benke, Marcin}
\index{Dybjer, Peter}
\index{Jansson, Patrik}
\begin{chunk}{axiom.bib}
@article{Benk03,
author = "Benke, Marcin and Dybjer, Peter and Jansson, Patrik",
title = "Universes for generic programs and proofs in dependent type
theory",
journal = "Nordic Journal of Computing",
volume = "10",
year = "2003",
pages = "265-269",
link = "\url{http://www.cse.chalmers.se/~peterd/papers/generic.html}",
abstract =
"We show how to write generic programs and proofs in {Martin L\"of}
type theory. To this end we considier several extensions of
{Martin-L\"of}'s logical framework for dependent types. Each extension
has a universe of codes (signatures) for inductively defined sets with
generic formation, introduction, elimination, and equality
rules. These extensions are modeled on Dybjer and Setzer's finitely
axiomatized theories of inductive-recursive definitions, which also
have universese of codes for sets, and generic formation,
introduction, elimination, and equality rules. Here we consider
several smaller universes of interest for generic programming and
universal algebra. We formalize one-sorted and many-sorted term
algebras, as well as iterated, generalized, parameterized, and indexed
inductive definitions. We also show how to extend the techniques of
generic programming to these universes. Furthermore, we give generic
proofs of reflexivity and substitutivity of a generic equality
test. Most of the definitions in the paper have been implemented using
the proof assistant Alfa for dependent type theory.",
paper = "Benk03.pdf"
}
\end{chunk}
\index{Martin-L\"of, Per}
\begin{chunk}{axiom.bib}
@misc{Mart80,
author = {Martin-L\"of, Per},
title = "Intuitionistic Type Theory",
link = "\url{http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf}",
year = "1980",
paper = "Mart80.pdf"
}
\end{chunk}
\index{Martin-L\"of, Per}
\begin{chunk}{axiom.bib}
@inproceedings{Mart85,
author = {Martin-L\"of, Per},
title = "Costructive Mathematics and Computer Programming",
booktitle = "Proc Royal Soc. of London on Math. Logic and Programming Lang.",
link = "\url{http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf}",
year = "1985",
isbn = "0-13-561465-1",
pages = "168-184",
publisher = "Prentice-Hall",
paper = "Mart85.pdf"
}
\end{chunk}
\index{Dybjer, Peter}
\index{Setzer, Anton}
\begin{chunk}{axiom.bib}
@article{Dybj03,
author = "Dybjer, Peter and Setzer, Anton",
title = "Induction-recursion and initial algebras",
journal = "Annals of Pure and Applied Logic",
volume = "124",
year = "2003",
pages = "1-47",
abstract =
"Induction-recursion is a powerful definition method in intuitionistic
type theory. It extends (generalized) inductive definitions and allows us
to define all standard sets of Martin-{L\"of} type theory as well as a
large collection of commonly occuring inductive data structures. It also
includes a variety of universes which are constructive analogues of
inaccessibles and other large cardinals below the first Mahlo cardinal.
In this article we give a new compact formalization of inductive-recursive
definnitions by modeling them as initial algebras in slice categories. We
give generic formation, introduction, elimination, and equality rules
generalizing the usual rules of type theory. Moreover, we prove that the
elimination and equality rules are equivalent to the principle of the
existence of initial algebras for certain endofunctors. We also show the
equivalence of the current formulation with the formulation of
induction-recursion as a reflection principle given in Dybjer and
Setzer (Lecture Notes in Comput. Sci. 2183 (2001) 93). Finally we discuss
two type-theoretic analogues of Mahlo cardinals in set theory: an external
Mahlo universe which is defined by induction-recursion and captured by our
formalization, and an internal Mahlo universe, which goes beyond induction-
recursion. We show that the external Mahlo universe, and therefore also
the theory of inductive-recursive definitions, have proof-theoretical
strength of at least Rathjen's theory KPM.",
paper = "Dybj03.pdf"
}
\end{chunk}
---
books/bookvolbib.pamphlet | 209 +++++++++++++++++++++++++++++++
changelog | 2 +
patch | 269 +++++++++++++++++++++++++++-------------
src/axiom-website/patches.html | 2 +
4 files changed, 393 insertions(+), 89 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 184d61a..bfe8a24 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -5579,6 +5579,42 @@ Martin, U.
\end{chunk}
+\index{Benke, Marcin}
+\index{Dybjer, Peter}
+\index{Jansson, Patrik}
+\begin{chunk}{axiom.bib}
+@article{Benk03,
+ author = "Benke, Marcin and Dybjer, Peter and Jansson, Patrik",
+ title = "Universes for generic programs and proofs in dependent type
+ theory",
+ journal = "Nordic Journal of Computing",
+ volume = "10",
+ year = "2003",
+ pages = "265-269",
+ link = "\url{http://www.cse.chalmers.se/~peterd/papers/generic.html}",
+ abstract =
+ "We show how to write generic programs and proofs in {Martin L\"of}
+ type theory. To this end we considier several extensions of
+ {Martin-L\"of}'s logical framework for dependent types. Each extension
+ has a universe of codes (signatures) for inductively defined sets with
+ generic formation, introduction, elimination, and equality
+ rules. These extensions are modeled on Dybjer and Setzer's finitely
+ axiomatized theories of inductive-recursive definitions, which also
+ have universese of codes for sets, and generic formation,
+ introduction, elimination, and equality rules. Here we consider
+ several smaller universes of interest for generic programming and
+ universal algebra. We formalize one-sorted and many-sorted term
+ algebras, as well as iterated, generalized, parameterized, and indexed
+ inductive definitions. We also show how to extend the techniques of
+ generic programming to these universes. Furthermore, we give generic
+ proofs of reflexivity and substitutivity of a generic equality
+ test. Most of the definitions in the paper have been implemented using
+ the proof assistant Alfa for dependent type theory.",
+ paper = "Benk03.pdf"
+}
+
+\end{chunk}
+
\index{Bertot, Yves}
\index{Cast\'eran, Pierre}
\begin{chunk}{axiom.bib}
@@ -5773,6 +5809,37 @@ Martin, U.
\end{chunk}
+\index{Bove, Ana}
+\index{Dybjer, Peter}
+\begin{chunk}{axiom.bib}
+@misc{Bove08,
+ author = "Bove, Ana and Dybjer, Peter",
+ title = "Dependent Types at Work",
+ year = "2008",
+ comment = "Lecture notes from LerNET Summer School, Piriapolis",
+ link =
+ "\url{http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf}",
+ abstract =
+ "In these lecture notes we give an introduction to functional
+ programming with dependent types. We use the dependently typed
+ programming language Agda which is an extension of {Martin-L\"of} type
+ theory. First we show how to do simply typed functional programming in
+ the style of Haskell and ML. Some differences between Agda's type
+ system and the Hindley-Milner type system of Haskell and ML are also
+ discussed. Then we show how to use dependent types for programming and
+ we explain the basic ideas behind type-checking dependent types. We go
+ on to explain the Curry-Howard identification of propositions and
+ types. This is what makes Agda a programming logic and not only a
+ programming language. According to Curry-Howard, we identify programs
+ and proofs, something which is possible only by requiring that all
+ programs terminate. However, at the end of these notes we present a
+ method for encoding partial and general recursive functions as total
+ functions using dependent types.",
+ paper = "Bove08.pdf"
+}
+
+\end{chunk}
+
\index{Bradley, Aaron R.}
\index{Manna, Zohar}
\begin{chunk}{axiom.bib}
@@ -6165,6 +6232,65 @@ England, Matthew; Wilson, David
\end{chunk}
+\index{Dybjer, Peter}
+\begin{chunk}{axiom.bib}
+@inproceedings{Dybj90,
+ author = "Dybjer, Peter",
+ title = {Inductive Sets and Families in Marin-L\"of's Type Theory and
+ Their Set-Theoretic Semantics},
+ booktitle = "Proc. First Workshop on Logical Frameworks",
+ year = "1990",
+ link =
+ "\url{http://www.cse.chalmers.se/~peterd/papers/Setsem\_Inductive.pdf}",
+ abstract =
+ "{Martin-L\"of}'s type theory is presented in several steps. The kernel
+ is a dependently typed $\lambda$-calculs. Then there are schemata for
+ inductive sets and families of sets and for primitive recursive functions
+ and families of functions. Finally, there are set formers (generic
+ polymorphism) and universes. At each step syntax, inference rules, and
+ set-theoretic sematics are given",
+ paper = "Dybj90.pdf"
+}
+
+\end{chunk}
+
+\index{Dybjer, Peter}
+\index{Setzer, Anton}
+\begin{chunk}{axiom.bib}
+@article{Dybj03,
+ author = "Dybjer, Peter and Setzer, Anton",
+ title = "Induction-recursion and initial algebras",
+ journal = "Annals of Pure and Applied Logic",
+ volume = "124",
+ year = "2003",
+ pages = "1-47",
+ abstract =
+ "Induction-recursion is a powerful definition method in intuitionistic
+ type theory. It extends (generalized) inductive definitions and allows us
+ to define all standard sets of Martin-{L\"of} type theory as well as a
+ large collection of commonly occuring inductive data structures. It also
+ includes a variety of universes which are constructive analogues of
+ inaccessibles and other large cardinals below the first Mahlo cardinal.
+ In this article we give a new compact formalization of inductive-recursive
+ definnitions by modeling them as initial algebras in slice categories. We
+ give generic formation, introduction, elimination, and equality rules
+ generalizing the usual rules of type theory. Moreover, we prove that the
+ elimination and equality rules are equivalent to the principle of the
+ existence of initial algebras for certain endofunctors. We also show the
+ equivalence of the current formulation with the formulation of
+ induction-recursion as a reflection principle given in Dybjer and
+ Setzer (Lecture Notes in Comput. Sci. 2183 (2001) 93). Finally we discuss
+ two type-theoretic analogues of Mahlo cardinals in set theory: an external
+ Mahlo universe which is defined by induction-recursion and captured by our
+ formalization, and an internal Mahlo universe, which goes beyond induction-
+ recursion. We show that the external Mahlo universe, and therefore also
+ the theory of inductive-recursive definitions, have proof-theoretical
+ strength of at least Rathjen's theory KPM.",
+ paper = "Dybj03.pdf"
+}
+
+\end{chunk}
+
\index{Dolzmann, Andreas}
\index{Sturm, Thomas}
\begin{chunk}{ignore}
@@ -6480,6 +6606,32 @@ Calculemus (2011) Springer
\end{chunk}
+\index{Goguen, Healfdene}
+\index{McBride, Conor}
+\index{McKinna, James}
+\begin{chunk}{axiom.bib}
+@article{Gogu06,
+ author = "Goguen, Healfdene and McBride, Conor and McKinna, James",
+ title = "Eliminating Dependent Pattern Matching",
+ year = "2006",
+ journal = "Lecture Notes in Computer Science",
+ volume = "4060",
+ pages = "521-540",
+ link = "\url{http://cs.ru.nl/~james/RESEARCH/goguen2006.pdf}",
+ abstract =
+ "This paper gives a reduction-preserving translation from Coquand's
+ {\sl dependent pattern matching} into a traditional type theory
+ with universes, inductive types and relations and the axiom K. This
+ translation serves as a proof of termination for structurally
+ recursive pattern matching programs, provides an implementable
+ compilation technique in the style of functional programming languages,
+ and demonstrates the equivelence with a more easily understood type
+ theory.",
+ paper = "Gogu06.pdf"
+}
+
+\end{chunk}
+
\index{Gottlieben, Hanne}
\index{Kelsey, Tom}
\index{Martin, Ursula}
@@ -6989,6 +7141,34 @@ Calculemus (2011) Springer
\index{Martin-L\"of, Per}
\begin{chunk}{axiom.bib}
+@misc{Mart80,
+ author = {Martin-L\"of, Per},
+ title = "Intuitionistic Type Theory",
+ link = "\url{http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf}",
+ year = "1980",
+ paper = "Mart80.pdf"
+}
+
+\end{chunk}
+
+\index{Martin-L\"of, Per}
+\begin{chunk}{axiom.bib}
+@inproceedings{Mart85,
+ author = {Martin-L\"of, Per},
+ title = "Costructive Mathematics and Computer Programming",
+ booktitle = "Proc Royal Soc. of London on Math. Logic and Programming Lang.",
+ link = "\url{http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf}",
+ year = "1985",
+ isbn = "0-13-561465-1",
+ pages = "168-184",
+ publisher = "Prentice-Hall",
+ paper = "Mart85.pdf"
+}
+
+\end{chunk}
+
+\index{Martin-L\"of, Per}
+\begin{chunk}{axiom.bib}
@article{Mart96,
author = {Martin-L\"of, Per},
title = "On the Meaning of the Logical Constants and the Justifications
@@ -7067,6 +7247,35 @@ Calculemus (2011) Springer
\end{chunk}
+\index{McBride, Conor}
+\index{Goguen, Healfdene}
+\index{McKinna, James}
+\begin{chunk}{axiom.bib}
+@article{Mcbr06,
+ author = "McBride, Conor and Goguen, Healfdene and McKinna, James",
+ title = "A Few Constructions on Constructors",
+ journal = "Lecture Notes in Computer Science",
+ volume = "3839",
+ pages = "186-200",
+ year = "2006",
+ link = "\url{http://www.strictlypositive.org/concon.ps.gz}",
+ abstract =
+ "We present four constructions for standard equipment which can be
+ generated for every inductive datatype: case analysis, structural
+ recursion, no confusion, acyclicity. Our constructions follow a
+ two-level approach -- they require less work than the standard
+ techniques which inspired them. Moreover, given a suitably
+ heterogeneous notion of equality, they extend without difficulty to
+ inductive families of datatypes. These constructions are vital
+ components of the translation from dependently typed programs in
+ pattern matching style to the equivalent programs expressed in terms
+ of induction principles and as such play a crucial behind-the-scenes
+ role in Epigram.",
+ paper = "Mcbr06.pdf"
+}
+
+\end{chunk}
+
\index{Mohring-Paulin, Christine}
\begin{chunk}{axiom.bib}
@misc{Mohr14,
diff --git a/changelog b/changelog
index 97616fa..366ae99 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20170220 tpd src/axiom-website/patches.html 20170220.01.tpd.patch
+20170220 tpd books/bookvolbib add additional references
20170215 tpd src/axiom-website/patches.html 20170215.01.tpd.patch
20170215 tpd books/bookheader.tex add Casteran and Sozeau to credits
20170215 tpd src/input/unittest1.input add Casteran and Sozeau to credits
diff --git a/patch b/patch
index 58ab829..1064b6f 100644
--- a/patch
+++ b/patch
@@ -2,121 +2,212 @@ books/bookvolbib add additional references
Goal: Proving Axiom Correct
-\index{Hoare, C. A. R.}
+\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
-@article{Hoar69,
- author = "Hoare, C. A. R.",
- title = "An Axiomatic Basis for Computer Programming",
- journal = "CACM",
- volume = "12",
- number = "10",
- pages = "576-580",
- year = "1969",
- link = "\url{https://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf}",
- abstract =
- "In this paper an attempt is made to explore the logical foundations
- of computer programming by use of techniques which were first applied
- in the study of geometry and have later been extended to other branches
- of mathematics. This involves the elucidation of sets of axioms and
- rules of inference which can be used in proofs of the properties of
- computer programs. Examples are given of such axioms and rules, and
- a formal proof of a simple theorem is displayed. Finally, it is argued
- that important advantages, both theoretical and practical, may follow
- from a pursuance of these topics",
- paper = "Hoar69.pdf"
+@inproceedings{Dybj90,
+ author = "Dybjer, Peter",
+ title = {Inductive Sets and Families in Marin-L\"of's Type Theory and
+ Their Set-Theoretic Semantics},
+ booktitle = "Proc. First Workshop on Logical Frameworks",
+ year = "1990",
+ link =
+ "\url{http://www.cse.chalmers.se/~peterd/papers/Setsem\_Inductive.pdf}",
+ abstract =
+ "{Martin-L\"of}'s type theory is presented in several steps. The kernel
+ is a dependently typed $\lambda$-calculs. Then there are schemata for
+ inductive sets and families of sets and for primitive recursive functions
+ and families of functions. Finally, there are set formers (generic
+ polymorphism) and universes. At each step syntax, inference rules, and
+ set-theoretic sematics are given",
+ paper = "Dybj90.pdf"
}
\end{chunk}
-\index{Casteran, Pierre}
-\index{Sozeau, Mattieu}
+\index{Goguen, Healfdene}
+\index{McBride, Conor}
+\index{McKinna, James}
\begin{chunk}{axiom.bib}
-@misc{Cast16,
- author = "Casteran, Pierre and Sozeau, Mattieu",
- title = "A Gentle Introduction to Type Classses and Relations in Coq",
- year = "2016",
- link = "\url{http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf}",
- paper = "Cast16.pdf"
+@article{Gogu06,
+ author = "Goguen, Healfdene and McBride, Conor and McKinna, James",
+ title = "Eliminating Dependent Pattern Matching",
+ year = "2006",
+ journal = "Lecture Notes in Computer Science",
+ volume = "4060",
+ pages = "521-540",
+ link = "\url{http://cs.ru.nl/~james/RESEARCH/goguen2006.pdf}",
+ abstract =
+ "This paper gives a reduction-preserving translation from Coquand's
+ {\sl dependent pattern matching} into a traditional type theory
+ with universes, inductive types and relations and the axiom K. This
+ translation serves as a proof of termination for structurally
+ recursive pattern matching programs, provides an implementable
+ compilation technique in the style of functional programming languages,
+ and demonstrates the equivelence with a more easily understood type
+ theory.",
+ paper = "Gogu06.pdf"
}
\end{chunk}
-\index{Sozeau, Mattieu}
+\index{McBride, Conor}
+\index{Goguen, Healfdene}
+\index{McKinna, James}
\begin{chunk}{axiom.bib}
-@inproceedings{Soze12,
- author = "Sozeau, Mattieu",
- title = "Coq with Classes",
- booktitle = "JFLA 2012",
- link = "\url{https://www.irif.fr/~sozeau/research/publications/Coq\_with\_Classes-JFLA-040212.pdf}",
- year = "2012",
- paper = "Soze12.pdf"
-}
+@article{Mcbr06,
+ author = "McBride, Conor and Goguen, Healfdene and McKinna, James",
+ title = "A Few Constructions on Constructors",
+ journal = "Lecture Notes in Computer Science",
+ volume = "3839",
+ pages = "186-200",
+ year = "2006",
+ link = "\url{http://www.strictlypositive.org/concon.ps.gz}",
+ abstract =
+ "We present four constructions for standard equipment which can be
+ generated for every inductive datatype: case analysis, structural
+ recursion, no confusion, acyclicity. Our constructions follow a
+ two-level approach -- they require less work than the standard
+ techniques which inspired them. Moreover, given a suitably
+ heterogeneous notion of equality, they extend without difficulty to
+ inductive families of datatypes. These constructions are vital
+ components of the translation from dependently typed programs in
+ pattern matching style to the equivalent programs expressed in terms
+ of induction principles and as such play a crucial behind-the-scenes
+ role in Epigram.",
+ paper = "Mcbr06.pdf"
+}
\end{chunk}
-\index{Bonichon, R.}
-\index{Delahaye, D.}
-\index{Doligez, D.}
+\index{Bove, Ana}
+\index{Dybjer, Peter}
\begin{chunk}{axiom.bib}
-@inproceedings{Boni07,
- author = "Bonichon, R. and Delahaye, D. and Doligez, D.",
- title = "Zenon: An Extensible Automated Theorem Prover Producing
- Checkable Proofs",
- booktitle = "LPAR 2007",
- year = "2007",
- link = "\url{http://zenon.inria.fr/zenlpar07.pdf}",
+@misc{Bove08,
+ author = "Bove, Ana and Dybjer, Peter",
+ title = "Dependent Types at Work",
+ year = "2008",
+ comment = "Lecture notes from LerNET Summer School, Piriapolis",
+ link =
+ "\url{http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf}",
abstract =
- "We present Zenon, an automated theorem prover for first order
- classical logic (with equality), based on the tableau method. Zenon is
- intended to be the dedicated prover of the Focal environment, an
- object-oriented algebraic specification and proof system, which is
- able to produce OCaml code for execution and Coq code for
- certification. Zenon can directly generate Coq proofs (proof scripts
- or proof terms), which can be reinserted in the Coq specifications
- produced by Focal. Zenon can also be extended, which makes specific
- (and possibly local) automation possible in Focal.",
- paper = "Boni07,pdf"
+ "In these lecture notes we give an introduction to functional
+ programming with dependent types. We use the dependently typed
+ programming language Agda which is an extension of {Martin-L\"of} type
+ theory. First we show how to do simply typed functional programming in
+ the style of Haskell and ML. Some differences between Agda's type
+ system and the Hindley-Milner type system of Haskell and ML are also
+ discussed. Then we show how to use dependent types for programming and
+ we explain the basic ideas behind type-checking dependent types. We go
+ on to explain the Curry-Howard identification of propositions and
+ types. This is what makes Agda a programming logic and not only a
+ programming language. According to Curry-Howard, we identify programs
+ and proofs, something which is possible only by requiring that all
+ programs terminate. However, at the end of these notes we present a
+ method for encoding partial and general recursive functions as total
+ functions using dependent types.",
+ paper = "Bove08.pdf"
}
\end{chunk}
-\index{Sozeau, Mattieu}
-\index{Oury, Nicolas}
+\index{Benke, Marcin}
+\index{Dybjer, Peter}
+\index{Jansson, Patrik}
\begin{chunk}{axiom.bib}
-@article{Soze08,
- author = "Sozeau, Mattieu and Oury, Nicolas",
- title = "First-Class Type Classes",
- journal = "Lecture Notes in Computer Science",
- volume = "5170",
- publisher = "Springer",
- year = "2008",
- pages = "278-293",
- link = "\url{https://www.irif.fr/~sozeau/research/publications/First-Class\_Type\_Classes.pdf}",
- abstract =
- "Type Classes have met a large success in Haskell and Isabelle, as a
- solution for sharing notations by overloading and for specifying with
- abstract structures by quantificaiton on contexts. However, both
- systems are limited by second-class implementations of these
- constructs, and these limitations are only overcome by ad-hoc
- extensions to the respective systems. We propose an embedding of type
- classes into a dependent type theory that is first-class and supports
- some of the most popular extensions right away. The implementation is
- correspondingly cheap, general, and integrates well inside the system,
- as we have experimented in Coq. We show how it can be used to help
- structured programming and proving by way of examples.",
- paper = "Soze08.pdf"
+@article{Benk03,
+ author = "Benke, Marcin and Dybjer, Peter and Jansson, Patrik",
+ title = "Universes for generic programs and proofs in dependent type
+ theory",
+ journal = "Nordic Journal of Computing",
+ volume = "10",
+ year = "2003",
+ pages = "265-269",
+ link = "\url{http://www.cse.chalmers.se/~peterd/papers/generic.html}",
+ abstract =
+ "We show how to write generic programs and proofs in {Martin L\"of}
+ type theory. To this end we considier several extensions of
+ {Martin-L\"of}'s logical framework for dependent types. Each extension
+ has a universe of codes (signatures) for inductively defined sets with
+ generic formation, introduction, elimination, and equality
+ rules. These extensions are modeled on Dybjer and Setzer's finitely
+ axiomatized theories of inductive-recursive definitions, which also
+ have universese of codes for sets, and generic formation,
+ introduction, elimination, and equality rules. Here we consider
+ several smaller universes of interest for generic programming and
+ universal algebra. We formalize one-sorted and many-sorted term
+ algebras, as well as iterated, generalized, parameterized, and indexed
+ inductive definitions. We also show how to extend the techniques of
+ generic programming to these universes. Furthermore, we give generic
+ proofs of reflexivity and substitutivity of a generic equality
+ test. Most of the definitions in the paper have been implemented using
+ the proof assistant Alfa for dependent type theory.",
+ paper = "Benk03.pdf"
}
\end{chunk}
-\index{Gries, David}
+\index{Martin-L\"of, Per}
\begin{chunk}{axiom.bib}
-@book{Grie81,
- author = "Gries, David",
- title = "The Science of Programming",
- publisher = "Springer-Verlag",
- year = "1981",
- isbn = "0-387-90641-X"
+@misc{Mart80,
+ author = {Martin-L\"of, Per},
+ title = "Intuitionistic Type Theory",
+ link = "\url{http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf}",
+ year = "1980",
+ paper = "Mart80.pdf"
}
\end{chunk}
+
+\index{Martin-L\"of, Per}
+\begin{chunk}{axiom.bib}
+@inproceedings{Mart85,
+ author = {Martin-L\"of, Per},
+ title = "Costructive Mathematics and Computer Programming",
+ booktitle = "Proc Royal Soc. of London on Math. Logic and Programming Lang.",
+ link = "\url{http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf}",
+ year = "1985",
+ isbn = "0-13-561465-1",
+ pages = "168-184",
+ publisher = "Prentice-Hall",
+ paper = "Mart85.pdf"
+}
+
+\end{chunk}
+
+\index{Dybjer, Peter}
+\index{Setzer, Anton}
+\begin{chunk}{axiom.bib}
+@article{Dybj03,
+ author = "Dybjer, Peter and Setzer, Anton",
+ title = "Induction-recursion and initial algebras",
+ journal = "Annals of Pure and Applied Logic",
+ volume = "124",
+ year = "2003",
+ pages = "1-47",
+ abstract =
+ "Induction-recursion is a powerful definition method in intuitionistic
+ type theory. It extends (generalized) inductive definitions and allows us
+ to define all standard sets of Martin-{L\"of} type theory as well as a
+ large collection of commonly occuring inductive data structures. It also
+ includes a variety of universes which are constructive analogues of
+ inaccessibles and other large cardinals below the first Mahlo cardinal.
+ In this article we give a new compact formalization of inductive-recursive
+ definnitions by modeling them as initial algebras in slice categories. We
+ give generic formation, introduction, elimination, and equality rules
+ generalizing the usual rules of type theory. Moreover, we prove that the
+ elimination and equality rules are equivalent to the principle of the
+ existence of initial algebras for certain endofunctors. We also show the
+ equivalence of the current formulation with the formulation of
+ induction-recursion as a reflection principle given in Dybjer and
+ Setzer (Lecture Notes in Comput. Sci. 2183 (2001) 93). Finally we discuss
+ two type-theoretic analogues of Mahlo cardinals in set theory: an external
+ Mahlo universe which is defined by induction-recursion and captured by our
+ formalization, and an internal Mahlo universe, which goes beyond induction-
+ recursion. We show that the external Mahlo universe, and therefore also
+ the theory of inductive-recursive definitions, have proof-theoretical
+ strength of at least Rathjen's theory KPM.",
+ paper = "Dybj03.pdf"
+}
+
+\end{chunk}
+
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 52da4dd..9f0488d 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5660,6 +5660,8 @@ books/bookvolbib Bradley and Manna The Calculus of Computation

readme add Jacob Nyffeler Smith to credits list

20170215.01.tpd.patch
books/bookvol13 add Binary Power in COQ chapter

+20170220.01.tpd.patch
+books/bookvolbib add additional references

--
1.7.5.4