Indexed categories for program development

Hilken, B.; Rydeheard, D. E.

Hilken, B. ; Rydeheard, D. E.

Cahiers de Topologie et Géométrie Différentielle Catégoriques, Tome 32 (1991) no. 2, pp. 165-185.

MR Zbl

@article{CTGDC_1991__32_2_165_0,
     author = {Hilken, B. and Rydeheard, D. E.},
     title = {Indexed categories for program development},
     journal = {Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle Cat\'egoriques},
     pages = {165--185},
     publisher = {Dunod \'editeur, publi\'e avec le concours du CNRS},
     volume = {32},
     number = {2},
     year = {1991},
     mrnumber = {1142689},
     zbl = {0746.03019},
     language = {en},
     url = {http://www.numdam.org/item/CTGDC_1991__32_2_165_0/}
}

TY  - JOUR
AU  - Hilken, B.
AU  - Rydeheard, D. E.
TI  - Indexed categories for program development
JO  - Cahiers de Topologie et Géométrie Différentielle Catégoriques
PY  - 1991
SP  - 165
EP  - 185
VL  - 32
IS  - 2
PB  - Dunod éditeur, publié avec le concours du CNRS
UR  - http://www.numdam.org/item/CTGDC_1991__32_2_165_0/
LA  - en
ID  - CTGDC_1991__32_2_165_0
ER  -

%0 Journal Article
%A Hilken, B.
%A Rydeheard, D. E.
%T Indexed categories for program development
%J Cahiers de Topologie et Géométrie Différentielle Catégoriques
%D 1991
%P 165-185
%V 32
%N 2
%I Dunod éditeur, publié avec le concours du CNRS
%U http://www.numdam.org/item/CTGDC_1991__32_2_165_0/
%G en
%F CTGDC_1991__32_2_165_0

Hilken, B.; Rydeheard, D. E. Indexed categories for program development. Cahiers de Topologie et Géométrie Différentielle Catégoriques, Tome 32 (1991) no. 2, pp. 165-185. http://www.numdam.org/item/CTGDC_1991__32_2_165_0/

Bibliographie
Cité par

Abramsky, S. (1987) Domain Theory in Logical Form. Proc. Symposium on Logic in Computer Science, June 22-25, I.E.E.E., Ithaca, NY.

Constable, R.L. et al. (1985) Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs, NJ.

Crole, R. & Pitts, A.M. (1990) New foundations for fixpoint computations. Proc. Symposium on Logic in Computer Science, June 4-7, 1990. I.E.E.E., Philadelphia, PA. | MR

Futatsugi, K., Goguen, J.A., Jouannaud, & Meseguer. (1985) Principles of OBJ2. In H.K. Reid (ed.) Proc. 12th ACM Symposium on Principles of Programming Languages, pp. 52-66. A.C.M.

Goguen, J.A. & Burstall, R.M. (1984) Introducing Institutions In E. Clarke and D. Kozen (eds) Logics of Programs, pp. 221-256, Springer LNCS 164. | MR | Zbl

Goldstine, H.H.& Von Neumann, J. (1947) "Planning and Coding of Problems for an Electronic Computing Instrument". Report of U.S. Ord. Dept. In A. Traub (ed.) Collected Works of J. von Neumann, New York, Pergamon, Vol. 5, pp 80-151. | MR

Gray, J.W., (1974) Formal Category Theory: Adjointness for 2-Categories. Springer LNM 391. | MR | Zbl

Harper, R., Honsell, F. & Plotkin, P. (1987) A Framework for Defining Logics. Proc. Symposium on Logic in Computer Science, June 22-25, I.E.E.E., Ithaca, NY.

Harper, R., Macqueen, D.B. AND Milner, R. (1986) Standard ML. Technical Report, ECS-LFCS-86-2, Edinburgh University, Department of Computer Science.

Hudak, P.& Wadler, P. et al. (1988) Report on the Functional Programming Language, Haskell. Draft proposed standard. Preprint, Dept. Computer Science, University of Glasgow, U.K.

Hyland, J.M.E. & Pitts, A.M. (1989) Theory of constructions: categorical semantics and topos-theoretic models. Proc. A.M.S. Conference on Categories in Computer Science and Logic, Boulder, Colorado (1987). A.M.S. | MR | Zbl

Johnstone, P.T. & Pare, R. (1978) (eds.) Indexed Categories and their Applications, Springer LMS 661. | MR | Zbl

Jones, C.B. (1986) Systematic Software Development Using VDM. Prentice-Hall International Series in Computer Science (ed. C.A.R. Hoare), Hemmel Hempstead. | Zbl

Kelly, G.M. (1982) Basic Concepts of Enriched Category Theory. London Math. Soc., Lecture Note Series, 64. C.U.P. | MR | Zbl

Lambek, J. & Scott, P.J. (1986) Introduction to higher order categorical logic. Cambridge studies in advanced mathematics 7. C.U.P. | MR | Zbl

Lawvere, F.W. (1969) Adjointness in Foundations. Dialectica 23, 3/4. pp. 281-296. | Zbl

Lawvere, F.W. (1970) Equality in Hyperdoctrines and the Comprehension Schema as an Adjoint Functor. Proc. Symp. in Pure Math., XVII: Applications of Categorical Algebra, A.M.S. pp 1-14. | MR | Zbl

Mac Lane, S. (1971) Categories for the Working Mathematician. Springer-Verlag, New York. | MR | Zbl

Manes, E.G. & Arbib, M.A. (1986) Algebraic Approaches to Program Semantics. Texts and Monographs in Computer Science, AKM Series, Springer-Verlag. | MR | Zbl

Martí-Oliet, N. & Meseguer, J. (1989) From Petri Nets to Linear Logic. Proc. Conference on Category Theory and Computer Science, Manchester, 1989, Springer LNCS 389. | MR

Moggi, E. (1989) Computational lambda-calculus and monads. Proc. 4th Symp. Logic in Computer Science, 1989, I.E.E.E. | Zbl

Moggi, E. (1989a) A categorical account of program modules. Proc. Summer Conference on Category Theory and Computer Science, Manchester 1989, Springer LNCS 389. | MR

Morris, F.L. & Jones, C.B. (1984) An Early Program Proof by Alan Turing. Annals of the History of Computing Vol. 6, Number 2, pp.139-143. | MR | Zbl

De Paiva, V.C.V. (1989) A Dialectica-like Model of Linear Logic. Proc. Summer Conference on Category Theory and Computer Science, Manchester 1989, Springer LNCS 389. | MR

Paulson, L.C. (1986) Natural deduction as higher-order resolution. J. Logic Programming, 3, pp. 237-258. | MR | Zbl

Pitts, A.M. (1987) Polymorphism is Set Theoretic, Constructively. Proc. Summer Conference on Category Theory and Computer Science, Edinburgh, 1987, Springer LNCS 283. | MR | Zbl

Rydeheard, D.E. & Burstall, R.M. (1988) Computational Category Theory. Prentice-Hall International Series in Computer Science (ed. C.A.R. Hoare), Hemmel Hempstead. | MR | Zbl

Rydeheard, D.E. & Stell, J.G. (1987) Foundations of Equational Deduction: A Categorical Treatment of Equational Proofs and Unification Algorithms. Proc. Summer Conference on Category Theory and Computer Science, Edinburgh, 1987, Springer LNCS 283. | MR | Zbl

Seely, R.A.G. (1983) Hyperdoctrines, Natural Deduction and the Beck Condition. Z. Math. Logik, 29, pp. 505-542. | MR | Zbl

Seely, R.A.G. (1984) Locally Cartesian Closed Categories and Type Theory. Math. Proc. Camb. Phil. Soc., 95, pp. 33-48. | MR | Zbl

Seely, R.A.G. (1987) Modelling Computations: A 2-Categorical Framework. Proc. Symp. Logic in Computer Science, June 22-25, 1987, I.E.E.E., Ithaca, NY.

Seely, R.A.G. (1987a) Categorical semantics for higher order polymorphic lambda calculus. J. Sym. Logic 52, 4. | MR | Zbl

Seely, R.A.G. (1987b) Linear Logic, *-Autonomous Categories and Cofree Co-algebras. In J.W. Gray and A. Scedrov (eds.), Proc. A.M.S. Conference on Categories in Computer Science and Logic, Boulder, Colorado. | Zbl

Street, R.H. (1974) Elementary Cosmoi. Springer LNM 420, pp. 104-133. | MR | Zbl

Street, R.H. (1976) Limits Indexed by Category-Valued 2-Functors. J. Pure and Applied Algebra, 8. pp. 149-181. | MR | Zbl

Turing, A.M. (1949) "Checking a Large Routine". In Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp. 67-69.