summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 30 Oct 1996 11:17:54 +0100 | |

changeset 2137 | afc15c2fd5b5 |

parent 2136 | 217ae06dc291 |

child 2138 | 056dead45ae8 |

Minor updates

--- a/doc-src/ind-defs.tex Wed Oct 30 11:15:09 1996 +0100 +++ b/doc-src/ind-defs.tex Wed Oct 30 11:17:54 1996 +0100 @@ -1,5 +1,5 @@ \documentstyle[a4,alltt,iman,extra,proof209,12pt]{article} -\newif\ifshort +\newif\ifshort%''Short'' means a published version, not the documentation \shortfalse%%%%%\shorttrue \title{A Fixedpoint Approach to\\ @@ -170,7 +170,8 @@ thus accepting all provably monotone inductive definitions, including iterated definitions. -The package has been implemented in Isabelle~\cite{isabelle-intro} using +The package has been implemented in +Isabelle~\cite{paulson-markt,paulson-isa-book} using \textsc{zf} set theory \cite{paulson-set-I,paulson-set-II}; part of it has since been ported to Isabelle/\textsc{hol} (higher-order logic). The recursion equations are specified as introduction rules for the mutually @@ -1299,9 +1300,10 @@ definitions (of arithmetic expressions, boolean expressions and commands) and three inductive definitions (the corresponding operational rules). Using different techniques, Nipkow~\cite{nipkow-CR} and Rasmussen~\cite{rasmussen95} -have both proved the Church-Rosser theorem. A datatype specifies the set of -$\lambda$-terms, while inductive definitions specify several reduction -relations. +have both proved the Church-Rosser theorem; inductive definitions specify +several reduction relations on $\lambda$-terms. Recently, I have applied +inductive definitions to the analysis of cryptographic +protocols~\cite{paulson-markt}. To demonstrate coinductive definitions, Frost~\cite{frost95} has proved the consistency of the dynamic and static semantics for a small functional