The following paper is available by anonymous FTP or over the Web Lambda Definability with Sums via Grothendieck Logical Relations by Marcelo Fiore and Alex Simpson We introduce a notion of *Grothendieck logical relation* and use it to characterise the definability of morphisms in *stable* bicartesian closed categories by terms of the simply-typed lambda calculus with finite products and finite sums. Our techniques are based on concepts from topos theory, however our exposition is elementary. The paper is written in a style appropriate for the conference Typed Lambda-Calculi and Applications where it is to be presented in April. However, we briefly discuss the true categorical content of the paper, which will be further expanded upon in a full version of the paper (forthcoming). The paper is available over the Web: http://www.dcs.ed.ac.uk/~mf/TYPES/glr.{dvi,ps} http://www.dcs.ed.ac.uk/~als/Research/glr.ps.gz or by anonymous FTP: ftp://ftp.dcs.ed.ac.uk/pub/mf/TYPES/glr.{dvi,ps} ftp://ftp.dcs.ed.ac.uk/pub/als/Research/glr.ps.gz Best wishes for a happy New Year, Alex Simpson -- Alex Simpson, LFCS, Division of Informatics, University of Edinburgh Email: Alex.Simpson@dcs.ed.ac.uk Tel: +44 (0)131 650 5113 FTP: ftp.dcs.ed.ac.uk/pub/als Fax: +44 (0)131 667 7209 URL: http://www.dcs.ed.ac.uk/home/als
The following paper is available by anonymous FTP or over the Web Computational Adequacy in an Elementary Topos We place simple axioms on an elementary topos which suffice for it to provide a denotational model of call-by-value PCF with sum and product types. The model is synthetic in the sense that types are interpreted by their set-theoretic counterparts within the topos. The main result characterises when the model is computationally adequate with respect to the operational semantics of the programming language. We prove that computational adequacy holds if and only if the topos is $1$-consistent (i.e. its internal logic validates only true $\Sigma^0_1$-sentences). This paper is to appear in the forthcoming proceedings of CSL 98. It is available from: http://www.dcs.ed.ac.uk/~als/Research/adequacy.ps.gz ftp://ftp.dcs.ed.ac.uk/pub/als/Research/adequacy.ps.gz Best wishes, Alex Simpson -- Alex Simpson, LFCS, Division of Informatics, University of Edinburgh Email: Alex.Simpson@dcs.ed.ac.uk Tel: +44 (0)131 650 5113 FTP: ftp.dcs.ed.ac.uk/pub/als Fax: +44 (0)131 667 7209 URL: http://www.dcs.ed.ac.uk/home/als
A heavily revised version of my paper "Beyond the Chu-construction" is now available from my home page: http://www.iti.cs.tu-bs.de/~koslowj/RESEARCH/ It will eventually be published in Applied Categorical Structures. I have not attempted to attribute the term "dualizing object" to anyone in particular. The open problem of an earlier version, as to whether Cauchy-complete bicategories of interpolads inherit local *-autonomy from their base, has been answered affirmatively. Here is the abstract: Starting from symmetric monoidal closed (= autonomous) categories, Po-Hsiang Chu showed how to construct new *-autonomous categories, i.e., autonomous categories that are self-dual because of a dualizing object. Recently, Michael Barr extended this to the non-symmetric, but closed, case, utilizing monads and modules between them. Since these notions are well-understood for bicategories, we introduce a notion of local *-autonomy for these that implies closedness and, moreover, is inherited when forming bicategories of monads and of interpolads. Since the initial step of Barr's construction also carries over to the bicategorical setting, we recover his main result as an easy corollary. Furthermore, the Chu-construction at this level may be viewed as a procedure for turning the endo-1-cells of a closed bicategory into the objects of a new closed bicategory, and hence conceptually is similar to constructing bicategories of monads and of interpolads. Best regards, -- J"urgen -- J"urgen Koslowski % If I don't see you no more in this world ITI % I meet you in the next world TU Braunschweig % and don't be late! koslowj@iti.cs.tu-bs.de % Jimi Hendrix (Voodoo Child)
participants (2)
-
Alex Simpson -
Koslowski