From megacz at cs.berkeley.edu Wed Jan 5 03:01:07 2011 From: megacz at cs.berkeley.edu (Adam Megacz) Date: Wed, 05 Jan 2011 08:01:07 +0000 Subject: [TYPES] System FC: inference rule (EqCo) and grammar for $\kappa$ Message-ID: Hello, I have a question about System FC, as described in the paper "System F with Type Equality Coercions" (Sulzmann, Chakravarty, Jones, Donnelly). Figure 3 describes the judgment $\vdash_k$, which is a ternary relation between a context, a kind, and a sort. Specifically, if we see a judgment: $$ X \vdash_k Y : Z $$ we know that X is from the syntactic class of contexts (nonterminal \Gamma of Figure 1), Y is from the syntactic class of kinds (nonterminal \kappa of Figure 1), and Z is from the syntactic class of sorts (nonterminal \delta of Figure 1). The first hypothesis of rule (EqCo) is $$ \Gamma \vdash_k \gamma_1 : CO $$ so we know that in rule (EqCo) $\gamma_1$ comes from the syntactic class of kinds. However, the conclusion of rule (EqCo) is: $$ \Gamma \vdash_k \gamma_1 \sim \gamma_2 : CO $$ We know that $\gamma_1 \sim \gamma_2$ is a kind, but in the $\kappa$ nonterminal in the grammar (Figure 1) the alternative for the $\sim$ operator indicates that its arguments -- in particular $\gamma_1$ -- must come from the syntactic class of types. This is in conflict with the previous paragraph. I suspect that the authors intended to have a fourth alternative for nonterminal $\kappa$, meaning that Figure 1 should be amended to: $$ \kappa,\iota \rightarrow \star | \kappa_1 \righatrrow \kappa_2 | \sigma_1 \sim \sigma_2 | \kappa_1 \sim \kappa_2 $$ Is my suspicion correct? If so, I believe the $\sim$ operator is actually triply-overloaded. I have a similar question about $\gamma$ in the conclusion of (CompC). Thanks, - a From simonpj at microsoft.com Tue Jan 11 18:03:32 2011 From: simonpj at microsoft.com (Simon Peyton-Jones) Date: Tue, 11 Jan 2011 23:03:32 +0000 Subject: [TYPES] System FC: inference rule (EqCo) and grammar for $\kappa$ In-Reply-To: References: Message-ID: <59543203684B2244980D7E4057D5FBC11F1EEB7D@DB3EX14MBXC308.europe.corp.microsoft.com> Adam The FC paper makes an elaborate pun between types and coercions. This is economical on notation, but it does my head in every time. Moreover, we treated the type (t1~t2) => t3 as syntactic sugar for forall (_ : t1~t2). t3 and that in turn leads directly to the confusion that you identify (I believe correctly). Rather than untangle that paper, have a look at our subsequent effort, "Generative type abstraction and type-level computation", to be presented at POPL later this month: http://www.cis.upenn.edu/~sweirich/newtypes.pdf There you'll see that (a) types and coercions are described separately, and (b) the type (t1~t2) => t3 is shorthand for a three-place type constructor (~e) t1 t2 t3. Despite some additional complexity from "roles" (introduced in this new paper), the result is a lot easier to grok, I think. You'll find a brief comparison with the old system in Section 6.2. best wishes Simon | -----Original Message----- | From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list- | bounces at lists.seas.upenn.edu] On Behalf Of Adam Megacz | Sent: 05 January 2011 08:01 | To: types-list at lists.seas.upenn.edu | Subject: [TYPES] System FC: inference rule (EqCo) and grammar for $\kappa$ | | [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] | | | Hello, I have a question about System FC, as described in the paper | "System F with Type Equality Coercions" (Sulzmann, Chakravarty, Jones, | Donnelly). | | Figure 3 describes the judgment $\vdash_k$, which is a ternary relation | between a context, a kind, and a sort. Specifically, if we see a | judgment: | | $$ X \vdash_k Y : Z $$ | | we know that X is from the syntactic class of contexts (nonterminal | \Gamma of Figure 1), Y is from the syntactic class of kinds (nonterminal | \kappa of Figure 1), and Z is from the syntactic class of sorts | (nonterminal \delta of Figure 1). | | The first hypothesis of rule (EqCo) is | | $$ \Gamma \vdash_k \gamma_1 : CO $$ | | so we know that in rule (EqCo) $\gamma_1$ comes from the syntactic class | of kinds. However, the conclusion of rule (EqCo) is: | | $$ \Gamma \vdash_k \gamma_1 \sim \gamma_2 : CO $$ | | We know that $\gamma_1 \sim \gamma_2$ is a kind, but in the $\kappa$ | nonterminal in the grammar (Figure 1) the alternative for the $\sim$ | operator indicates that its arguments -- in particular $\gamma_1$ -- | must come from the syntactic class of types. This is in conflict with | the previous paragraph. | | I suspect that the authors intended to have a fourth alternative for | nonterminal $\kappa$, meaning that Figure 1 should be amended to: | | $$ \kappa,\iota | \rightarrow | \star | | \kappa_1 \righatrrow \kappa_2 | | \sigma_1 \sim \sigma_2 | | \kappa_1 \sim \kappa_2 | $$ | | Is my suspicion correct? If so, I believe the $\sim$ operator is | actually triply-overloaded. | | I have a similar question about $\gamma$ in the conclusion of (CompC). | | Thanks, | | - a | | From fruehr at willamette.edu Sat Jan 15 03:38:14 2011 From: fruehr at willamette.edu (Fritz Ruehr) Date: Sat, 15 Jan 2011 00:38:14 -0800 Subject: [TYPES] Time for types-as-arithmetic, by analogy with types-as-propositions? Message-ID: <4E847F41-C810-4A51-A91C-D446BBF48ADD@willamette.edu> Over the last few years I have noticed a trend of research which draws an analogy between types (on the one hand) and numbers and arithmetic (on the other): "type arithmetic" (calculation of type isomorphisms), derivatives of data types, generating functions and power series related to types, etc. (Details and references are relegated below.) I wonder if it is time for more overt recognition of a "types-as-arithmetic" analogy, like the celebrated types-as-propositions correspondence. Does anyone else recognize this as a trend? Do you think it is worthy of more focused attention, or even just a better, community-endorsed slogan? On a more formal level, types (under iso-equivalence), propositions and arithmetic all fit into (versions of) Tarski's "high school identities", as models of an abstract algebra with a nice, structured axiomatization. I have used the pithier term "power rings", since they extend a commutative semi-ring (for sums and products) with exponentials and related laws (e.g., corresponding to currying and to categorical sums and products). (There are, of course, problems with bottom / non-termination in some computational interpretations, just as for Curry-Howard^H^H^H^H, uhh, types-as-propositions.) Am I merely glimpsing what others (more categorically sophisticated, no doubt) take for granted? Is there an existing terminology for (or a more elaborated literature around) this analogy between types and arithmetic? Perhaps this is all just about bicartesian closed categories, but I don't see differentiation and some other ideas described in this context. In addition to reactions on the general idea, I would also appreciate any pointers to other work which might fall under this rubric. -- Fritz Ruehr -------------------------- Ideas, papers and blog posts that exemplify the "types-as-arithmetic" trend include: * The folklore idea of "type arithmetic", in which one calculates types equivalent up to isomorphism by using the usual "high school identities" about addition, multiplication and exponentiation, but interpreting them in terms of disjoint sum, cartesian product and function space. * Roberto Di Cosmo's use of these equivalences in his work on type isomorphism [DiC95] (he specifically recognized the relevance of Tarski's identities in this context). * Application of type arithmetic to the memoization of functions as tries in work by Ralf Hinze [Hin00ab]; see also related work and extensions by Conal Elliott [Ell08] and Dan Piponi [Pip09a]. * Conor McBride's work on the differentiation of data types [McB01], where the usual rules for derivatives are re-interpreted for types and shown to correspond to the notion of datatype context used in Huet's zipper construction (see also Conor's "Clowns and Jokers" work on dissection [McB06], which Dan Piponi recognizes [Pip09b] as corresponding to finite differences). * Notions of subtraction, division and differentiation for the combinatorial species of Joyal [Joy81]; species can in some ways be seen as an extension or generalization of algebraic datatypes. See Brent Yorgey's Haskell Workshop paper [Yor10a] and his blog [Yor10b] for an introduction to species in the context of functional programming and to "virtual species" in particular. Subtraction and division are apparently definable for types by the same Grothendieck construction which generalizes the extension of the naturals to the integers and rationals. Parts of this "trend" go back much further than the past few years: already in William Burge's book "Recursive Programming Techniques" [Bur75] we see the use of generating functions and power series as a way to think about data types. (There is apparently some related work by Corrado Boehm and Maria Dezani-Ciancaglini [BDC74] dating to 1974, although I don't have easy access to a copy.) I have myself advocated for a more explicit use of "type arithmetic" in the pedagogy of functional programming [Rue08], as well as for more recognition and study of the corresponding abstract algebra I call "power rings". References: [BDC74] A data structure formalization through generating functions. Corrado Boehm and Maria Dezani-Ciancaglini, Calcolo vol. 11(#1), Springer, 1974. [Bur75] Recursive Programming Techniques, William H. Burge, The Systems programming series, Addison-Wesley, 1975. [diC95] Isomorphisms of types: from lambda calculus to information retrieval and language design. Roberto Di Cosmo, Birkhauser, 1995. [Ell08] Elegant memoization with functional memo tries. Conal Elliott, blog post at URL , 2008. [Hin00a] Generalizing generalized tries. Ralf Hinze, Journal of Functional Programming, vol. 10(#4), Cambridge, 2000. [Hin00b] Memo functions, polytypically! Ralf Hinze, WGP '00 (Ponte de Lima), ACM, 2000. [Joy81] Une theorie combinatoire des series formelles. Andre Joyal, Advances in Mathematics vol 42, 1981. [McB01] The Derivative of a Regular Type is its Type of One-Hole Contexts. Conor McBride, available from the author's page at , 2001. [McB06] Clowns to the left of me, jokers to the right. Conor McBride, available from the author's page at , 2006. [Pip09a] Memoizing Polymorphic Functions with High School Algebra and Quantifiers. Dan Piponi (sigfpe), A Neighborhood of Infinity, blog post at URL , 2009. [Pip09b] Finite Differences of Types. Dan Piponi (sigfpe), A Neighborhood of Infinity, blog post at URL , 2009. [Rue08] Tips on Teaching Types and Functions. Fritz Ruehr, FDPE '08 (Victoria), ACM, 2008. [Yor10a] Species and functors and types, oh my! Brent Yorgey, Haskell '10 (Baltimore), ACM, 2010. [Yor10b] Species subtraction made simple. Brent Yorgey, blog :: Brent -> [String], blog post at URL , 2010. From florian.lorenzen at tu-berlin.de Mon Jun 6 12:07:32 2011 From: florian.lorenzen at tu-berlin.de (Florian Lorenzen) Date: Mon, 06 Jun 2011 18:07:32 +0200 Subject: [TYPES] System F omega with (equi-)recursive types Message-ID: <1307376452.2168.12.camel@gilgalad> Dear types forum members, I have been looking for publications studying the properties (type safety, decidability of type checking, type checking algorithm) of System F omega combined with (equi-)recursive types but have, unfortunately, been quite unsuccessful. I am interested in an extension of F omega where the X in (mu X. T) ranges over proper types of kind *. I would very much appreciate any pointers into the literature. Thank you and best regards, Florian -- Florian Lorenzen Technische Universit?t Berlin Fakult?t IV - Elektrotechnik und Informatik ?bersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen at tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz From Francois.Pottier at inria.fr Mon Jun 6 17:00:41 2011 From: Francois.Pottier at inria.fr (Francois Pottier) Date: Mon, 6 Jun 2011 23:00:41 +0200 Subject: [TYPES] System F omega with (equi-)recursive types In-Reply-To: <745194868.1374061.1307377980979.JavaMail.root@zmbs2.inria.fr> References: <745194868.1374061.1307377980979.JavaMail.root@zmbs2.inria.fr> Message-ID: <20110606210041.GC9582@yquem.inria.fr> Hello, On Mon, Jun 06, 2011 at 06:33:00PM +0200, Florian Lorenzen wrote: > I have been looking for publications studying the properties (type > safety, decidability of type checking, type checking algorithm) of > System F omega combined with (equi-)recursive types but have, > unfortunately, been quite unsuccessful. I am interested in an extension > of F omega where the X in (mu X. T) ranges over proper types of kind *. First, do you know about the papers that concern System F with equi-recursive types? There is a paper by Neal Glew and one by Nadji Gauthier and I on efficiently deciding type equality in the presence of \forall and \mu quantifiers. You can find references to earlier work in there (e.g. work by Colazzo and Ghelli). Once you know how to check type equality, the rest (proof of type soundness, type-checking algorithm) is just as in System F; the presence of recursive types has essentially no impact. You say that you are interested in System F_omega, but you restrict the \mu quantifier to variables of kind *. It seems to me that the resulting system remains fairly simple, because beta-reduction and the unfolding of \mu's cannot interact: unfolding a \mu cannot cause a beta-redex to appear. Thus, you should be able to first bring every type to a normal form, as in Ssytem F_omega, then compare types for equality, as in System F with recursive types. If you allow \mu at every kind, things become more interesting. There is an old paper by Marvin Solomon at POPL 1978 where it is showed that in the presence of parameterized, recursive types definitions (that is, in System F_omega with \mu at every kind), deciding whether two types are equal is equivalent to the then-open problem of deciding whether two deterministic pushdown automata are equivalent. This problem has been shown to be decidable since then, but no practical/tractable algorithm exists, as far as I understand. The more recent paper by Stone and Schoonmaker is probably very relevant (I haven't read it). The fun becomes greater yet if you allow not just recursive types at every kind, but recursive kinds to begin with. Then, the Y fixed point combinator can be defined at the level of types (it is well-kinded), so the notion of a recursive type need not be considered primitive: \mu X.T can be viewed as syntactic sugar for Y (\lambda X.T). I have considered a system based on this somewhat exotic idea in my POPL 2011 paper. Up to some restrictions (which ensure that every recursive type definition is productive in a certain sense) the problem of determining whether two types are equal is semi-decidable. (I don't know if it is decidable.) I have implemented a type-checker, which is available online. The proof of type soundness (which appears in the long version of the paper) is completely standard: again, it is not affected by the presence of recursive types. Basically, all you need in order to prove subject reduction is injectivity of type constructors (e.g., A -> B = C -> D implies A = C and B = D), and all you need in order to prove progress is disjointness of type constructors (e.g., A -> B != C * D). These properties are usually easily shown to hold, even in the presence of recursive types. Oh, and you also need reflexivity and transitivity of type equality, which (depending on your definition of equality and depending on how non-trivial an equational theory you want to bake in) could be somewhat tricky to prove in the presence of recursive types. It is very likely that there are important references concerning recursive types that I have not mentioned here; I apologize for that. I hope nevertheless that this is useful, -- Fran?ois Pottier Francois.Pottier at inria.fr http://gallium.inria.fr/~fpottier/ From frederic.blanqui at inria.fr Mon Jun 6 20:16:30 2011 From: frederic.blanqui at inria.fr (Frederic Blanqui) Date: Tue, 07 Jun 2011 08:16:30 +0800 Subject: [TYPES] System F omega with (equi-)recursive types In-Reply-To: <1307376452.2168.12.camel@gilgalad> References: <1307376452.2168.12.camel@gilgalad> Message-ID: <4DED6DDE.7040506@inria.fr> For termination, you may have a look at: Strong Normalization and Equi-(co)inductive Types Andreas Abel /Typed Lambda Calculi and Application, TLCA'07. Best regards, Frederic. / Le 07/06/2011 00:07, Florian Lorenzen a ?crit : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > > Dear types forum members, > > I have been looking for publications studying the properties (type > safety, decidability of type checking, type checking algorithm) of > System F omega combined with (equi-)recursive types but have, > unfortunately, been quite unsuccessful. I am interested in an extension > of F omega where the X in (mu X. T) ranges over proper types of kind *. > > I would very much appreciate any pointers into the literature. > > Thank you and best regards, > > Florian > From Sam.Lindley at ed.ac.uk Sun Oct 9 18:39:06 2011 From: Sam.Lindley at ed.ac.uk (Sam Lindley) Date: Sun, 09 Oct 2011 23:39:06 +0100 Subject: [TYPES] F omega with sums and commuting conversions Message-ID: <4E92228A.7010102@ed.ac.uk> Is there a published strong normalisation proof for F omega extended with coproduct types and commuting conversions? Sam -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. From andreas.abel at ifi.lmu.de Mon Oct 10 08:04:55 2011 From: andreas.abel at ifi.lmu.de (Andreas Abel) Date: Mon, 10 Oct 2011 14:04:55 +0200 Subject: [TYPES] F omega with sums and commuting conversions In-Reply-To: <4E92228A.7010102@ed.ac.uk> References: <4E92228A.7010102@ed.ac.uk> Message-ID: <4E92DF67.20508@ifi.lmu.de> Hello Sam, Ralph Matthes has written (APAL 133, pp. 205-230, 2005) A manuscript on "Non-Strictly Positive Fixed-Points for Classical Natural Deduction" http://www.irit.fr/~Ralph.Matthes/works.html which contains system F^+ with commuting conversions as a subsystem. The SN proof scales to Fomega. Cheers, Andreas On 10/10/11 12:39 AM, Sam Lindley wrote: > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Is there a published strong normalisation proof for F omega extended > with coproduct types and commuting conversions? > > Sam > -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel at ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/ From carette at mcmaster.ca Thu Oct 13 11:23:54 2011 From: carette at mcmaster.ca (Jacques Carette) Date: Thu, 13 Oct 2011 11:23:54 -0400 Subject: [TYPES] Types for Open Terms ? Message-ID: <4E97028A.1050706@mcmaster.ca> I have been looking to find relevant work on types for open terms, i.e. types for terms with free variables which are *not* in an environment. I have been able to find some work by Westbrook [1], Geuvers and Jojgov [2], Geuvers, Krebbers, McKinna and Wiedijk [3] directly on this, as well as depply inside Sacerdoti Coen's thesis [4]. It appears that and Nanevski, Pfenning and Pientka [5]'s contextual modal type theory is "related" (but scary in its complexity...), as compared say with Rhiger's much simpler system [6] which seems to offer similar benefits as far as my needs go. What have I missed? Jacques [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf [3] http://arxiv.org/abs/1009.2792v1 [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz [5] http://dl.acm.org/citation.cfm?id=1352591 [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf From anthony.de.almeida.lopes at falsifiable.net Thu Oct 13 11:58:56 2011 From: anthony.de.almeida.lopes at falsifiable.net (Anthony de Almeida Lopes) Date: Thu, 13 Oct 2011 16:58:56 +0100 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E97028A.1050706@mcmaster.ca> References: <4E97028A.1050706@mcmaster.ca> Message-ID: "A Typed Context Calculus" - www.pllab.riec.tohoku.ac.jp/~ohori/research/contcalc.pdf These are possibly less related but they both develop similar open-term systems: http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.4045 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.4514&rank=1 I beleive that this is the final product of the above two: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.346&rank=1 At one time Conor McBride gave me quite a good list to follow up which I don't have it on me right now, but I think the main author was actually Jojgov. It looks like he may have more to offer for you: http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/j/Jojgov:Gueorgui_I=.html Good luck, - Anthony 2011/10/13 Jacques Carette : > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I have been looking to find relevant work on types for open terms, i.e. > types for terms with free variables which are *not* in an environment. > > I have been able to find some work by Westbrook [1], Geuvers and Jojgov [2], > Geuvers, Krebbers, McKinna and Wiedijk [3] directly on this, as well as > depply inside Sacerdoti Coen's thesis [4]. ?It appears that and Nanevski, > Pfenning and Pientka [5]'s contextual modal type theory is "related" (but > scary in its complexity...), as compared say with Rhiger's much simpler > system [6] which seems to offer similar benefits as far as my needs go. > > What have I missed? > > Jacques > > [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf > [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf > [3] http://arxiv.org/abs/1009.2792v1 > [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz > [5] http://dl.acm.org/citation.cfm?id=1352591 > [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf > > > From anthony.de.almeida.lopes at falsifiable.net Thu Oct 13 13:48:38 2011 From: anthony.de.almeida.lopes at falsifiable.net (Anthony de Almeida Lopes) Date: Thu, 13 Oct 2011 18:48:38 +0100 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E9722AF.5020109@ropas.snu.ac.kr> References: <4E97028A.1050706@mcmaster.ca> <4E9722AF.5020109@ropas.snu.ac.kr> Message-ID: 2011/10/13 Kwangkeun Yi : > One missing paper is > "A Polymorphic Modal Type System for Lisp-Like Multi-Staged > Languages"(POPL'06) > http://ropas.snu.ac.kr/~kwang/paper/06-jfp-yi.pdf > > Best, > > -Kwang I think you meant http://www.doc.ic.ac.uk/~ccris/ftp/06-popl-kiyicr.pdf From nicolas.pouillard at gmail.com Thu Oct 13 16:14:28 2011 From: nicolas.pouillard at gmail.com (Nicolas Pouillard) Date: Thu, 13 Oct 2011 22:14:28 +0200 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E97028A.1050706@mcmaster.ca> References: <4E97028A.1050706@mcmaster.ca> Message-ID: On Thu, Oct 13, 2011 at 5:23 PM, Jacques Carette wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Hello, > I have been looking to find relevant work on types for open terms, i.e. > types for terms with free variables which are *not* in an environment. Our work with Fran?ois Pottier should be relevant for what you are looking for. Our approach has been described in a first paper [1], a second paper [2] presents a nicer system studying the de Bruijn approach more in depth. My PhD thesis would soon be available as well. It contains the nicer presentation of our second paper but unified to various first-order representations: nominal, de Bruijn indices, de Bruijn levels and combinations of them. Best regards, -- Nicolas Pouillard http://nicolaspouillard.fr [1]: ?A Fresh Look at Programming With Names and Binders? (ICFP 2010) http://nicolaspouillard.fr/#fresh-look-paper [2]: ?Nameless, Painless? (ICFP 2011) http://nicolaspouillard.fr/#nameless-painless From herman at cs.ru.nl Fri Oct 14 03:37:41 2011 From: herman at cs.ru.nl (Herman Geuvers) Date: Fri, 14 Oct 2011 09:37:41 +0200 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E97028A.1050706@mcmaster.ca> References: <4E97028A.1050706@mcmaster.ca> Message-ID: <4E97E6C5.4040701@cs.ru.nl> Dear Jacques Carette, Apart from this there is also the PhD thesis og Jojgov, that I can't find on-line anywhere. Georgi Jojgov, Incomplete proofs and terms and their use in interactive theorem proving (PhD thesis, Eindhoven 2004) I will send you a copy of it via surface mail and I'll contact Jojgov whether he has it in electronic form somewhere. Best Herman Geuvers > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I have been looking to find relevant work on types for open terms, > i.e. types for terms with free variables which are *not* in an > environment. > > I have been able to find some work by Westbrook [1], Geuvers and > Jojgov [2], Geuvers, Krebbers, McKinna and Wiedijk [3] directly on > this, as well as depply inside Sacerdoti Coen's thesis [4]. It > appears that and Nanevski, Pfenning and Pientka [5]'s contextual modal > type theory is "related" (but scary in its complexity...), as compared > say with Rhiger's much simpler system [6] which seems to offer similar > benefits as far as my needs go. > > What have I missed? > > Jacques > > [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf > [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf > [3] http://arxiv.org/abs/1009.2792v1 > [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz > [5] http://dl.acm.org/citation.cfm?id=1352591 > [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf > -- Herman Geuvers Professor of Computer Science Intelligent Systems, iCIS Faculty of Science Radboud University Nijmegen, NL From asperti at cs.unibo.it Fri Oct 14 04:40:47 2011 From: asperti at cs.unibo.it (Andrea Asperti) Date: Fri, 14 Oct 2011 10:40:47 +0200 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E97E6C5.4040701@cs.ru.nl> References: <4E97028A.1050706@mcmaster.ca> <4E97E6C5.4040701@cs.ru.nl> Message-ID: <4E97F58F.1020501@cs.unibo.it> Dear Jacques, if I understood what you are looking for, you could also be interested in recent paper (under submission) by myself, Ricciotti, Sacerdoti Coen and Tassi, entitled "A bidirectional refinement algorithm for the Calculus of (Co)Inductive Constructions". I'll send you a copy by email. Best. -- andrea Herman Geuvers wrote: > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Jacques Carette, > > Apart from this there is also the PhD thesis og Jojgov, that I can't > find on-line anywhere. > > Georgi Jojgov, > Incomplete proofs and terms and their use in interactive theorem > proving (PhD thesis, Eindhoven 2004) > > I will send you a copy of it via surface mail and I'll contact Jojgov > whether he has it in electronic form somewhere. > > Best > > Herman Geuvers > >> [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> I have been looking to find relevant work on types for open terms, >> i.e. types for terms with free variables which are *not* in an >> environment. >> >> I have been able to find some work by Westbrook [1], Geuvers and >> Jojgov [2], Geuvers, Krebbers, McKinna and Wiedijk [3] directly on >> this, as well as depply inside Sacerdoti Coen's thesis [4]. It >> appears that and Nanevski, Pfenning and Pientka [5]'s contextual >> modal type theory is "related" (but scary in its complexity...), as >> compared say with Rhiger's much simpler system [6] which seems to >> offer similar benefits as far as my needs go. >> >> What have I missed? >> >> Jacques >> >> [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf >> [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf >> [3] http://arxiv.org/abs/1009.2792v1 >> [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz >> [5] http://dl.acm.org/citation.cfm?id=1352591 >> [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf >> > > From bellissimogiorno at gmail.com Sat Oct 15 06:47:36 2011 From: bellissimogiorno at gmail.com (murdoch gabbay) Date: Sat, 15 Oct 2011 11:47:36 +0100 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E97028A.1050706@mcmaster.ca> References: <4E97028A.1050706@mcmaster.ca> Message-ID: Dear Jaques, You might like to glance at the following: "Principal types for nominal theories" http://gabbay.org.uk/papers.html#printn "Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms" http://gabbay.org.uk/papers.html#curhif-jv "Lambda-context calculus" http://gabbay.org.uk/papers.html#lamcce Murdoch Gabbay On 13 October 2011 16:23, Jacques Carette wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list] > > I have been looking to find relevant work on types for open terms, i.e. > types for terms with free variables which are *not* in an environment. From bpientka at cs.mcgill.ca Sat Oct 15 13:17:06 2011 From: bpientka at cs.mcgill.ca (Brigitte Pientka) Date: Sat, 15 Oct 2011 13:17:06 -0400 Subject: [TYPES] Types for Open Terms ? In-Reply-To: <4E97028A.1050706@mcmaster.ca> References: <4E97028A.1050706@mcmaster.ca> Message-ID: Dear Jacques, thank you for your interest in open terms and types! You may want to take a look at our work on Beluga which allows users to program with open terms. It may give you a more accessible way for playing with and understanding contextual objects. A Prototype for download is available at http://complogic.cs.mcgill.ca/beluga/ [Pientka 2008] A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Brigitte Pientka, 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 371-382, ACM Press, 2008. [Cave, Pientka 2012] Programming with Binders and Indexed Data-types, Andrew Cave and Brigitte Pientka, accepted at 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12) For gentle introductions: Beluga: programming with dependent types, contextual data, and contexts,Brigitte Pientka, Invited talk at 10th International Symposium on Functional and Logic Programming (FLOPS'10), April 2010, Sendai, Japan. Programming inductive proofs: a new approach based on contextual types, Brigitte Pientka, Verification, Induction, and Termination analysis, LNAI, Springer, Aug 2010 Best wishes, - Brigitte On Thu, Oct 13, 2011 at 11:23 AM, Jacques Carette wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > I have been looking to find relevant work on types for open terms, i.e. > types for terms with free variables which are *not* in an environment. > > I have been able to find some work by Westbrook [1], Geuvers and Jojgov [2], > Geuvers, Krebbers, McKinna and Wiedijk [3] directly on this, as well as > depply inside Sacerdoti Coen's thesis [4]. ?It appears that and Nanevski, > Pfenning and Pientka [5]'s contextual modal type theory is "related" (but > scary in its complexity...), as compared say with Rhiger's much simpler > system [6] which seems to offer similar benefits as far as my needs go. > > What have I missed? > > Jacques > > [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf > [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf > [3] http://arxiv.org/abs/1009.2792v1 > [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz > [5] http://dl.acm.org/citation.cfm?id=1352591 > [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf > > From adam at poswolsky.com Sat Oct 15 16:32:22 2011 From: adam at poswolsky.com (Adam Poswolsky) Date: Sat, 15 Oct 2011 16:32:22 -0400 Subject: [TYPES] Types for Open Terms ? In-Reply-To: References: <4E97028A.1050706@mcmaster.ca> Message-ID: Wow.? I'm also glad to see a renewed interest in open terms! I would like to point out my work with Carsten Schuermann on the Delphin Project where we created a dependently-typed languages which supports HOAS. Please see the website here:? http://cs-www.cs.yale.edu/homes/delphin/. You can download the system.? The latest version is 1.5.1 and it is a full release so everything is implemented including the coverage and termination checker so the system will tell you if any cases are missing or if the program may not terminate. My dissertation explains the entire system starting with a simply-typed version to gently explain the novelty in how we represent open terms. http://www.cs.yale.edu/homes/poswolsk/papers/poswolsky-dissertation.pdf For a quick read, I suggest Adam Poswolsky and Carsten Sch?rmann. ?Practical Programming with Higher-Order Encodings and Dependent Types. ?In European Symposium on Programming (ESOP 2008) http://www.cs.yale.edu/homes/poswolsk/papers/delphinESOP08.pdf The main novelty of our work in compared with the context-based approaches are that just as in HOAS the context remains implicit, we keep the context implicit and allow the user to reason over open terms by just keeping track of the relative differences in the context.? In particular, the type Nabla(x).Nabla(y).T represents a type T where both x and y occur free. If you are interested and have any other questions please don't hesitate to ask. Cheers, Adam On Sat, Oct 15, 2011 at 1:17 PM, Brigitte Pientka wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Dear Jacques, > > ?thank you for your interest in open terms and types! > > You may want to take a look at our work on Beluga which allows users > to program with open terms. It may give you a more accessible way for > playing with and understanding contextual objects. > > A Prototype for download is available at ?http://complogic.cs.mcgill.ca/beluga/ > > [Pientka 2008] A type-theoretic foundation for programming with > higher-order abstract syntax and first-class substitutions, Brigitte > Pientka, 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of > Programming Languages (POPL'08), pages 371-382, ACM Press, 2008. > > [Cave, Pientka 2012] Programming with Binders and Indexed Data-types, > Andrew Cave and Brigitte Pientka, accepted at 39th ACM SIGPLAN-SIGACT > Symposium on Principles of Programming Languages (POPL'12) > > For gentle introductions: > > Beluga: programming with dependent types, contextual data, and > contexts,Brigitte Pientka, Invited talk at 10th International > Symposium on Functional and Logic Programming (FLOPS'10), April 2010, > Sendai, Japan. > > Programming inductive proofs: a new approach based on contextual > types, Brigitte Pientka, Verification, Induction, and Termination > analysis, LNAI, Springer, Aug 2010 > > > Best wishes, > > - Brigitte > > > On Thu, Oct 13, 2011 at 11:23 AM, Jacques Carette wrote: >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> I have been looking to find relevant work on types for open terms, i.e. >> types for terms with free variables which are *not* in an environment. >> >> I have been able to find some work by Westbrook [1], Geuvers and Jojgov [2], >> Geuvers, Krebbers, McKinna and Wiedijk [3] directly on this, as well as >> depply inside Sacerdoti Coen's thesis [4]. ?It appears that and Nanevski, >> Pfenning and Pientka [5]'s contextual modal type theory is "related" (but >> scary in its complexity...), as compared say with Rhiger's much simpler >> system [6] which seems to offer similar benefits as far as my needs go. >> >> What have I missed? >> >> Jacques >> >> [1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf >> [2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf >> [3] http://arxiv.org/abs/1009.2792v1 >> [4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz >> [5] http://dl.acm.org/citation.cfm?id=1352591 >> [6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf >> >> > From emw4 at rice.edu Thu Nov 3 12:15:09 2011 From: emw4 at rice.edu (Eddy Westbrook) Date: Thu, 3 Nov 2011 11:15:09 -0500 Subject: [TYPES] Strong Normalization for Coq (CiC) Message-ID: <63BEF68F-5DBA-4244-AED3-F283E7D5A044@rice.edu> All, I have a new generalization of logical relations that can prove SN for CiC (the core theory of Coq), including the full universe hierarchy and inductive types. AFAIK, this has been an open problem for a while, and I thought my solution would be of interest to people on this list. The basic idea is uniformity, where, instead of defining an interpretation (aka a logical relation) for only types, or defining one for types and one for terms, in my approach the interpretation is defined uniformly on all terms M. When M happens to be a type, the interpretation is similar to the standard logical relations for types. The current draft can be found here: http://www.cs.rice.edu/~emw4/uniform-lr.pdf Thanks in advance for any input! -Eddy P.S. Thanks again to everyone who has helped me out with this paper, including prior anonymous reviewers. From decoy at iki.fi Mon Nov 7 13:54:13 2011 From: decoy at iki.fi (Sampo Syreeni) Date: Mon, 7 Nov 2011 20:54:13 +0200 (EET) Subject: [TYPES] Strong Normalization for Coq (CiC) In-Reply-To: <63BEF68F-5DBA-4244-AED3-F283E7D5A044@rice.edu> References: <63BEF68F-5DBA-4244-AED3-F283E7D5A044@rice.edu> Message-ID: On 2011-11-03, Eddy Westbrook wrote: > The basic idea is uniformity, where, instead of defining an > interpretation (aka a logical relation) for only types, or defining > one for types and one for terms, in my approach the interpretation is > defined uniformly on all terms M. When M happens to be a type, the > interpretation is similar to the standard logical relations for types. > > The current draft can be found here: > http://www.cs.rice.edu/~emw4/uniform-lr.pdf Will read, but prima facie, how precisely do you avoid the kinds of level problems and self-circularity which lead to type hierarchies in the first place, if you just treat the levels as categorically equivalent? This is an idiot-question, I know, but I also feel it's the first one to be answered in this kind of unifying work. -- Sampo Syreeni, aka decoy - decoy at iki.fi, http://decoy.iki.fi/front +358-50-5756111, 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2 From bernardy at chalmers.se Tue Nov 8 08:02:48 2011 From: bernardy at chalmers.se (Jean-Philippe Bernardy) Date: Tue, 8 Nov 2011 14:02:48 +0100 Subject: [TYPES] Strong Normalization for Coq (CiC) Message-ID: Hello, I should point out that in [1], we have given a notion of logical relation which is uniformly defined for terms, types and sorts. Although we stay away from the problem of normalization, the definition follows a similar pattern as yours. You might also be interested in glancing at [2] or even [3]. Cheers, JP. [1] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=118913 [2] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466 [3] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=147257 From emw4 at rice.edu Tue Nov 8 18:09:40 2011 From: emw4 at rice.edu (Eddy Westbrook) Date: Tue, 8 Nov 2011 17:09:40 -0600 Subject: [TYPES] Strong Normalization for Coq (CiC) In-Reply-To: References: Message-ID: <719C2EC7-4B58-4966-ACEA-F9800F00D173@rice.edu> Excellent, thanks very much for the references! I will definitely cite them in my work. -E On Nov 8, 2011, at 7:02 AM, Jean-Philippe Bernardy wrote: > Hello, > > I should point out that in [1], we have given a notion of logical > relation > which is uniformly defined for terms, types and sorts. Although we > stay away from > the problem of normalization, the definition follows a similar > pattern as yours. > > You might also be interested in glancing at [2] or even [3]. > > Cheers, > JP. > > [1] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=118913 > [2] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466 > [3] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=147257 > From emw4 at rice.edu Tue Nov 8 18:20:39 2011 From: emw4 at rice.edu (Eddy Westbrook) Date: Tue, 8 Nov 2011 17:20:39 -0600 Subject: [TYPES] Strong Normalization for Coq (CiC) In-Reply-To: References: <63BEF68F-5DBA-4244-AED3-F283E7D5A044@rice.edu> Message-ID: Yes, this is a very fundamental question. This is discussed more in the paper, but the basic answer is that I use a "dummy" interpretation for proofs, which is essentially like the empty set; i.e., the interpretations of proofs do not "contain" any other terms (where "contain" is in a set-theoretic sense). Thus, the interpretation of Prop and its types can be built before any of the predicative types. This may seem counter-intuitive at first, because proofs can contain predicative objects. The reason it works, however, is that the only way to get predicative objects out of a proof is via an impredicative elimination, which must always, in the end, create another proof. Thus, such functions always equal \dummy -> dummy, which we in fact eta-contract in the interpretation function to just dummy. Hope this helps, -Eddy On Nov 7, 2011, at 12:54 PM, Sampo Syreeni wrote: > On 2011-11-03, Eddy Westbrook wrote: > >> The basic idea is uniformity, where, instead of defining an >> interpretation (aka a logical relation) for only types, or defining >> one for types and one for terms, in my approach the interpretation >> is defined uniformly on all terms M. When M happens to be a type, >> the interpretation is similar to the standard logical relations for >> types. >> >> The current draft can be found here: >> http://www.cs.rice.edu/~emw4/uniform-lr.pdf > > Will read, but prima facie, how precisely do you avoid the kinds of > level problems and self-circularity which lead to type hierarchies > in the first place, if you just treat the levels as categorically > equivalent? This is an idiot-question, I know, but I also feel it's > the first one to be answered in this kind of unifying work. > -- > Sampo Syreeni, aka decoy - decoy at iki.fi, http://decoy.iki.fi/front > +358-50-5756111, 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2 > From roconnor at theorem.ca Thu Nov 17 15:57:36 2011 From: roconnor at theorem.ca (roconnor at theorem.ca) Date: Thu, 17 Nov 2011 15:57:36 -0500 (EST) Subject: [TYPES] Representing inductive types with W-types Message-ID: Does anyone have a reference on how to encode (non-mutually recursive) inductive data type declarations of a language similar to CiC using W-Types? I was playing around with this by hand, and I can make ad-hoc encodings for the types I've tried; but I haven't quite figured out what the systematic translation is. For example, I find Inductive Tree (A:Type) : Type := node : A -> list (Tree A) -> Tree A quite difficult to translate. I can only manage because I happen to know that list X ~ Sigma n:nat. Fin n -> X where Fin Fin 0 = Void Fin (S n) = Unit + Fin n By my ad hoc method I get nat ~ W : Bool. if b then Void else Unit list A ~ W x : Unit + A. [const Void | const Unit] x Tree A ~ W (a,n):A*nat. Fin n But of course nat and Fin do not directly appear in the Inductive definition of Tree, so I'm not entirely sure how to deduce them (or something isomorphic) systematically. -- Russell O'Connor ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' From sojakova.kristina at gmail.com Thu Nov 17 17:50:43 2011 From: sojakova.kristina at gmail.com (Kristina Sojakova) Date: Thu, 17 Nov 2011 17:50:43 -0500 Subject: [TYPES] Representing inductive types with W-types Message-ID: <4EC58FC3.3090501@gmail.com> Dear Russell, I do not necessarily see anything ad-hoc about the particular encoding of tress as Tree A ~ W (a,n):A*nat. Fin n On the other hand, I find it very natural. After all, a tree is determined by 1) a term a : A, which is the value at the root 2) a term n : nat, which is the number of children 3) n subtrees Each pair (a,n) will determine a separate constructor, thus the type of constructors will be A x nat. Since the arity of the constructor (a,n) is n, we need a dependent type (a,n) : A x nat |- B(a,n) type such that B(a,n) is inhabited by exactly n terms. As we see the value of a does not matter for this requirement, thus we need a type n : nat |- B(n) type which is inhabited by precisely n terms, which is the specification of Fin(n). You are right that the types nat and Fin do not occur in the Coq definition of Tree A explicitly and have to be inferred at the meta-level. So if you are asking whether it is possible to derive a completely generic way to encode suitable data types (as in, a precise algorithm) then the answer is probably not. There has been some work done by Gambino&Hyland in their paper "Wellfounded trees and Dependent Polynomial Functors": http://www.math.unipa.it/~ngambino/Research/Papers/gambino-hyland.pdf They show that certain class of inductive types corresponding to the dependent polynomial functors can be represented by W-types (which correspond to non-dependent polynomial functors). I am not sure if this is what you were looking for though. Best, Kristina From peterd at chalmers.se Fri Nov 18 02:41:39 2011 From: peterd at chalmers.se (Peter Dybjer) Date: Fri, 18 Nov 2011 08:41:39 +0100 Subject: [TYPES] Representing inductive types with W-types In-Reply-To: References: Message-ID: <994D40AD62B42647972DD232E960C85535756376AF@MAPI01.ita.chalmers.se> Dear Russell, "Does anyone have a reference on how to encode (non-mutually recursive) inductive data type declarations of a language similar to CiC using W-Types?" Have a look at http://www.cse.chalmers.se/~peterd/papers/Wellorderings.pdf Best wishes, Peter From roconnor at theorem.ca Sun Nov 20 15:38:47 2011 From: roconnor at theorem.ca (roconnor at theorem.ca) Date: Sun, 20 Nov 2011 15:38:47 -0500 (EST) Subject: [TYPES] Representing inductive types with W-types In-Reply-To: References: Message-ID: Does this mean that containers are "the same" as strictly positive functors? Because all strictly postive functors are isomorphic to some container, and every container is a strictly positive functor? On Thu, 17 Nov 2011, Altenkirch Thorsten wrote: > Hi Russell, > > I think our work on containers is relevant here. You can show that any > strictly positive functor can be represented as a container, I.e. A > functor of the form > F X = Sigma s:S. P s -> X where S : Set, P : S -> Set, I.e. the signature > of a W-type. > Actually for your example you need n-ary containers to handle nested types. > > The relevant results are in our '05 Journal paper > http://www.cs.nott.ac.uk/~txa/publ/cont-tcs.pdf > And in Michael Abbot's PhD. > > Recently (with Peter Morris) we extended this to dependent types, this > appeared in LICS 2009 http://www.cs.nott.ac.uk/~txa/publ/ICont.pdf > > Cheers, > Thorsten > > On 17/11/2011 20:57, "roconnor at theorem.ca" wrote: > >> [ The Types Forum, >> http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Does anyone have a reference on how to encode (non-mutually recursive) >> inductive data type declarations of a language similar to CiC using >> W-Types? >> >> I was playing around with this by hand, and I can make ad-hoc encodings >> for the types I've tried; but I haven't quite figured out what the >> systematic translation is. For example, I find >> >> Inductive Tree (A:Type) : Type := >> node : A -> list (Tree A) -> Tree A >> >> quite difficult to translate. I can only manage because I happen to know >> that list X ~ Sigma n:nat. Fin n -> X >> >> where Fin >> >> Fin 0 = Void >> Fin (S n) = Unit + Fin n >> >> By my ad hoc method I get >> >> nat ~ W : Bool. if b then Void else Unit >> list A ~ W x : Unit + A. [const Void | const Unit] x >> Tree A ~ W (a,n):A*nat. Fin n >> >> But of course nat and Fin do not directly appear in the Inductive >> definition of Tree, so I'm not entirely sure how to deduce them (or >> something isomorphic) systematically. >> >> -- >> Russell O'Connor >> ``All talk about `theft,''' the general counsel of the American >> Graphophone >> Company wrote, ``is the merest claptrap, for there exists no property in >> ideas musical, literary or artistic, except as defined by statute.'' > > This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. > > This message has been checked for viruses but the contents of an attachment > may still contain software viruses which could damage your computer system: > you are advised to perform your own checks. Email communications with the > University of Nottingham may be monitored as permitted by UK legislation. -- Russell O'Connor ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''