--- a/Pearl-jv/Paper.thy Tue Mar 01 00:14:02 2011 +0000
+++ b/Pearl-jv/Paper.thy Wed Mar 02 00:06:28 2011 +0000
@@ -1,7 +1,6 @@
(*<*)
theory Paper
imports "../Nominal/Nominal2_Base"
- "../Nominal/Nominal2_Eqvt"
"../Nominal/Atoms"
"../Nominal/Nominal2_Abs"
"LaTeXsugar"
@@ -41,15 +40,11 @@
(*>*)
-(*
- TODO: write about supp of finite sets, abstraction over finite sets
-*)
-
section {* Introduction *}
text {*
Nominal Isabelle provides a proving infratructure for convenient reasoning
- about programming language calculi involving binders such as lambda abstractions or
+ about programming language calculi involving binders, such as lambda abstractions or
quantifications in type schemes:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -59,129 +54,14 @@
\noindent
At its core Nominal Isabelle is based on the nominal logic work by Pitts at
- al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
+ al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a
sort-respecting permutation operation defined over a countably infinite
- collection of sorted atoms. The atoms are used for representing variable names
- that might be bound or free. Multiple sorts are necessary for being able to
- represent different kinds of variables. For example, in the language Mini-ML
- there are bound term variables in lambda abstractions and bound type variables in
- type schemes. In order to be able to separate them, each kind of variables needs to be
- represented by a different sort of atoms.
-
- The existing nominal logic work usually leaves implicit the sorting
- information for atoms and as far as we know leaves out a description of how
- sorts are represented. In our formalisation, we therefore have to make a
- design decision about how to implement sorted atoms and sort-respecting
- permutations. One possibility, which we described in \cite{Urban08}, is to
- have separate types for the different
- kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
- design one can represent permutations as lists of pairs of atoms and the
- operation of applying a permutation to an object as the function
-
-
- @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-
- \noindent
- where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
- of the objects on which the permutation acts. For atoms
- the permutation operation is defined over the length of lists as follows
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
- @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
- $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
- @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
- @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
- \end{tabular}\hfill\numbered{atomperm}
- \end{isabelle}
-
- \noindent
- where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
- @{text "b"}. For atoms with different type than the permutation, we
- define @{text "\<pi> \<bullet> c \<equiv> c"}.
-
- With the separate atom types and the list representation of permutations it
- is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
- permutation, since the type system excludes lists containing atoms of
- different type. However, a disadvantage is that whenever we need to
- generalise induction hypotheses by quantifying over permutations, we have to
- build quantifications like
-
- @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
-
- \noindent
- where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
- The reason is that the permutation operation behaves differently for
- every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
- single quantification to stand for all permutations. Similarly, the
- notion of support
-
- @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-
- \noindent
- which we will define later, cannot be
- used to express the support of an object over \emph{all} atoms. The reason
- is that support can behave differently for each @{text
- "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
- a statement that an object, say @{text "x"}, is finitely supported we end up
- with having to state premises of the form
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
- \end{tabular}\hfill\numbered{fssequence}
- \end{isabelle}
-
- \noindent
- Because of these disadvantages, we will use in this paper a single unified atom type to
- represent atoms of different sorts. Consequently, we have to deal with the
- case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
- the type systems to exclude them.
-
- We also will not represent permutations as lists of pairs of atoms (as done in
- \cite{Urban08}). Although an
- advantage of this representation is that the basic operations on
- permutations are already defined in Isabelle's list library: composition of
- two permutations (written @{text "_ @ _"}) is just list append, and
- inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
- list reversal, and another advantage is that there is a well-understood
- induction principle for lists, a disadvantage is that permutations
- do not have unique representations as lists. We have to explicitly identify
- them according to the relation
+ collection of sorted atoms. The nominal logic work has been starting
+ point for a number of formalisations, most notable Norrish \cite{norrish04}
+ in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own
+ work in Isabelle/HOL.
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
- \end{tabular}\hfill\numbered{permequ}
- \end{isabelle}
-
- \noindent
- This is a problem when lifting the permutation operation to other types, for
- example sets, functions and so on. For this we need to ensure that every definition
- is well-behaved in the sense that it satisfies some
- \emph{permutation properties}. In the list representation we need
- to state these properties as follows:
-
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
- i) & @{text "[] \<bullet> x = x"}\\
- ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
- iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
- \end{tabular}\hfill\numbered{permprops}
- \end{isabelle}
-
- \noindent
- where the last clause explicitly states that the permutation operation has
- to produce the same result for related permutations. Moreover,
- ``permutations-as-lists'' do not satisfy the group properties. This means by
- using this representation we will not be able to reuse the extensive
- reasoning infrastructure in Isabelle about groups. Because of this, we will represent
- in this paper permutations as functions from atoms to atoms. This representation
- is unique and satisfies the laws of non-commutative groups.
-
Using a single atom type to represent atoms of different sorts and
representing permutations as functions are not new ideas; see
\cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution
@@ -199,6 +79,24 @@
section {* Sorted Atoms and Sort-Respecting Permutations *}
text {*
+ The most basic notion in this work is a
+ sort-respecting permutation operation defined over a countably infinite
+ collection of sorted atoms. The atoms are used for representing variable names
+ that might be bound or free. Multiple sorts are necessary for being able to
+ represent different kinds of variables. For example, in the language Mini-ML
+ there are bound term variables in lambda abstractions and bound type variables in
+ type schemes. In order to be able to separate them, each kind of variables needs to be
+ represented by a different sort of atoms.
+
+
+ The existing nominal logic work usually leaves implicit the sorting
+ information for atoms and as far as we know leaves out a description of how
+ sorts are represented. In our formalisation, we therefore have to make a
+ design decision about how to implement sorted atoms and sort-respecting
+ permutations. One possibility, which we described in \cite{Urban08}, is to
+ have separate types for the different
+ kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
+
In the nominal logic work of Pitts, binders and bound variables are
represented by \emph{atoms}. As stated above, we need to have different
\emph{sorts} of atoms to be able to bind different kinds of variables. A
@@ -314,7 +212,7 @@
@{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
@{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
@{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
- @{thm diff_def[where M="\<pi>\<^isub>1" and N="\<pi>\<^isub>2"]}
+ @{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
\end{tabular}
\end{isabelle}
@@ -1202,184 +1100,123 @@
*}
-section {* Multi-Sorted Concrete Atoms *}
-
-(*<*)
-datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _")
-(*>*)
-
-text {*
- The formalisation presented so far allows us to streamline proofs and reduce
- the amount of custom ML-code in the existing implementation of Nominal
- Isabelle. In this section we describe a mechanism that extends the
- capabilities of Nominal Isabelle. This mechanism is about variables with
- additional information, for example typing constraints.
- While we leave a detailed treatment of binders and binding of variables for a
- later paper, we will have a look here at how such variables can be
- represented by concrete atoms.
-
- In the previous section we considered concrete atoms that can be used in
- simple binders like \emph{@{text "\<lambda>x. x"}}. Such concrete atoms do
- not carry any information beyond their identities---comparing for equality
- is really the only way to analyse ordinary concrete atoms.
- However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
- underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
- more complicated structure. For example in the ``Church-style'' lambda-term
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
- \end{tabular}\hfill\numbered{church}
- \end{isabelle}
-
- \noindent
- both variables and binders include typing information indicated by @{text \<alpha>}
- and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
- "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
- variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
- @{text "x\<^isub>\<beta>"}.
-
- To illustrate how we can deal with this phenomenon, let us represent object
- types like @{text \<alpha>} and @{text \<beta>} by the datatype
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- \isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the
- problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
- will always permute \emph{both} occurrences of @{text x}, even if the types
- @{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
- eventually mean that both occurrences of @{text x} will become bound by a
- corresponding binder.
-
- Another attempt might be to define variables as an instance of the concrete
- atom type class, where a @{text ty} is somehow encoded within each variable.
- Remember we defined atoms as the datatype:
-*}
-
- datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-
-text {*
- \noindent
- Considering our method of defining concrete atom types, the usage of a string
- for the sort of atoms seems a natural choice. However, none of the results so
- far depend on this choice and we are free to change it.
- One possibility is to encode types or any other information by making the sort
- argument parametric as follows:
-*}
-
- datatype 'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat
-
-text {*
- \noindent
- The problem with this possibility is that we are then back in the old
- situation where our permutation operation is parametric in two types and
- this would require to work around Isabelle/HOL's restriction on type
- classes. Fortunately, encoding the types in a separate parameter is not
- necessary for what we want to achieve, as we only have to know when two
- types are equal or not. The solution is to use a different sort for each
- object type. Then we can use the fact that permutations respect \emph{sorts} to
- ensure that permutations also respect \emph{object types}. In order to do
- this, we must define an injective function @{text "sort_ty"} mapping from
- object types to sorts. For defining functions like @{text "sort_ty"}, it is
- more convenient to use a tree datatype for sorts. Therefore we define
-*}
-
- datatype sort = Sort string "(sort list)"
- datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
-
-text {*
- \noindent
- With this definition,
- the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
- The point, however, is that we can now define the function @{text sort_ty} simply as
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
- @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
- \end{tabular}\hfill\numbered{sortty}
- \end{isabelle}
-
- \noindent
- which can easily be shown to be injective.
-
- Having settled on what the sorts should be for ``Church-like'' atoms, we have to
- give a subtype definition for concrete atoms. Previously we identified a subtype consisting
- of atoms of only one specified sort. This must be generalised to all sorts the
- function @{text "sort_ty"} might produce, i.e.~the
- range of @{text "sort_ty"}. Therefore we define
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
- \end{isabelle}
-
- \noindent
- This command gives us again injective representation and abstraction
- functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
- @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively.
-
- We can define the permutation operation for @{text var} as @{thm
- permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
- injective function to type @{typ atom} as @{thm atom_var_def[THEN
- eq_reflection, no_vars]}. Finally, we can define a constructor function that
- makes a @{text var} from a variable name and an object type:
-
- @{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}
-
- \noindent
- With these definitions we can verify all the properties for concrete atom
- types except Property \ref{atomprops}@{text ".iii)"}, which requires every
- atom to have the same sort. This last property is clearly not true for type
- @{text "var"}.
- This fact is slightly unfortunate since this
- property allowed us to use the type-checker in order to shield the user from
- all sort-constraints. But this failure is expected here, because we cannot
- burden the type-system of Isabelle/HOL with the task of deciding when two
- object types are equal. This means we sometimes need to explicitly state sort
- constraints or explicitly discharge them, but as we will see in the lemma
- below this seems a natural price to pay in these circumstances.
-
- To sum up this section, the encoding of type-information into atoms allows us
- to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following
- lemma
-*}
-
- lemma
- assumes asm: "\<alpha> \<noteq> \<beta>"
- shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
- using asm by simp
-
-text {*
- \noindent
- As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
- swapping. With this we can faithfully represent bindings in languages
- involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
- expect that the creation of such atoms can be easily automated so that the
- user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
- where the argument, or arguments, are datatypes for which we can automatically
- define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
- Our hope is that with this approach Benzmueller and Paulson can make
- headway with formalising their results
- about simple type theory \cite{PaulsonBenzmueller}.
- Because of its limitations, they did not attempt this with the old version
- of Nominal Isabelle. We also hope we can make progress with formalisations of
- HOL-based languages.
-*}
section {* Related Work *}
text {*
Add here comparison with old work.
-
The main point is that the above reasoning blends smoothly with the reasoning
infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
type class suffices.
+
+ With this
+ design one can represent permutations as lists of pairs of atoms and the
+ operation of applying a permutation to an object as the function
+
+
+ @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+ \noindent
+ where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
+ of the objects on which the permutation acts. For atoms
+ the permutation operation is defined over the length of lists as follows
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+ @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
+ $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
+ @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
+ @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
+ \end{tabular}\hfill\numbered{atomperm}
+ \end{isabelle}
+
+ \noindent
+ where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
+ @{text "b"}. For atoms with different type than the permutation, we
+ define @{text "\<pi> \<bullet> c \<equiv> c"}.
+
+ With the separate atom types and the list representation of permutations it
+ is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
+ permutation, since the type system excludes lists containing atoms of
+ different type. However, a disadvantage is that whenever we need to
+ generalise induction hypotheses by quantifying over permutations, we have to
+ build quantifications like
+
+ @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
+
+ \noindent
+ where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
+ The reason is that the permutation operation behaves differently for
+ every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
+ single quantification to stand for all permutations. Similarly, the
+ notion of support
+
+ @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
+
+ \noindent
+ which we will define later, cannot be
+ used to express the support of an object over \emph{all} atoms. The reason
+ is that support can behave differently for each @{text
+ "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
+ a statement that an object, say @{text "x"}, is finitely supported we end up
+ with having to state premises of the form
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
+ \end{tabular}\hfill\numbered{fssequence}
+ \end{isabelle}
+
+ \noindent
+ Because of these disadvantages, we will use in this paper a single unified atom type to
+ represent atoms of different sorts. Consequently, we have to deal with the
+ case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
+ the type systems to exclude them.
+
+ We also will not represent permutations as lists of pairs of atoms (as done in
+ \cite{Urban08}). Although an
+ advantage of this representation is that the basic operations on
+ permutations are already defined in Isabelle's list library: composition of
+ two permutations (written @{text "_ @ _"}) is just list append, and
+ inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
+ list reversal, and another advantage is that there is a well-understood
+ induction principle for lists, a disadvantage is that permutations
+ do not have unique representations as lists. We have to explicitly identify
+ them according to the relation
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
+ \end{tabular}\hfill\numbered{permequ}
+ \end{isabelle}
+
+ \noindent
+ This is a problem when lifting the permutation operation to other types, for
+ example sets, functions and so on. For this we need to ensure that every definition
+ is well-behaved in the sense that it satisfies some
+ \emph{permutation properties}. In the list representation we need
+ to state these properties as follows:
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+ i) & @{text "[] \<bullet> x = x"}\\
+ ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
+ iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
+ \end{tabular}\hfill\numbered{permprops}
+ \end{isabelle}
+
+ \noindent
+ where the last clause explicitly states that the permutation operation has
+ to produce the same result for related permutations. Moreover,
+ ``permutations-as-lists'' do not satisfy the group properties. This means by
+ using this representation we will not be able to reuse the extensive
+ reasoning infrastructure in Isabelle about groups. Because of this, we will represent
+ in this paper permutations as functions from atoms to atoms. This representation
+ is unique and satisfies the laws of non-commutative groups.
*}
--- a/Pearl-jv/document/root.bib Tue Mar 01 00:14:02 2011 +0000
+++ b/Pearl-jv/document/root.bib Wed Mar 02 00:06:28 2011 +0000
@@ -8,6 +8,17 @@
year = "2008"
}
+@InProceedings{norrish04,
+ author = {M.~Norrish},
+ title = {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders},
+ booktitle = {Proc.~of the 17th International Conference Theorem Proving in
+ Higher Order Logics (TPHOLs)},
+ pages = {241--256},
+ year = {2004},
+ volume = {3223},
+ series = {LNCS}
+}
+
@InProceedings{GunterOsbornPopescu09,
author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu},
title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in
@@ -19,6 +30,16 @@
series = {ENTCS}
}
+@InProceedings{AydemirBohannonWeirich07,
+ author = {B.~Aydemir and A.~Bohannon and S.~Weihrich},
+ title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)},
+ booktitle = {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages:
+ Theory and Practice (LFMTP)},
+ pages = {69--77},
+ year = {2007},
+ series = {ENTCS}
+}
+
@Unpublished{SatoPollack10,
author = {M.~Sato and R.~Pollack},
title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},