zbMATH — the first resource for mathematics

Notions of computation and monads. (English) Zbl 0723.68073
Summary: The \(\lambda\)-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with \(\lambda\)-terms. However, if one goes further and uses \(\beta\eta\)- conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results.
We introduce calculi, based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation.

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
Full Text: DOI
[1] Barr, M.; Wells, C., ()
[2] Crole, R.L.; Pitts, A.M., New foundations for fixpoint computations, () · Zbl 0763.03031
[3] Constable, R.L.; Smith, S.F., Partial objects in constructive type theory, ()
[4] Constable, R.L.; Smith, S.F., Computational foundations of basic recursive function theory, () · Zbl 0798.03046
[5] Felleisen, M.; Friedman, D.P., A syntactic theory of sequential state, Theoret. comput. sci., 69, No. 3, (1989) · Zbl 0688.68014
[6] Felleisen, M.; Friedman, D.P.; Kohlbecker, E.; Duba, B., Reasoning with continuations, ()
[7] Fourman, M.P., The logic of topoi, () · Zbl 0415.03053
[8] Gordon, M.J.C.; Milner, R.; Wadsworth, C.P., Edinburgh LCF: A mechanized logic of computation, () · Zbl 0421.68039
[9] Gunter, C.; Scott, S., (), [To appear in North-Holland Handbook of Theoretical Computer Science]
[10] Harper, R.; Mitchell, J.; Moggi, E., Higher-order modules and the phase distinction, ()
[11] Hyland, J.M.E.; Pitts, A.M., The theory of constructions: categorical semantics and topos-theoretic models, () · Zbl 0721.03048
[12] ()
[13] Kelly, G.M., ()
[14] Kock, A., Strong functors and monoidal monads, Arch. math., 23, (1972) · Zbl 0253.18007
[15] Kock, A.; Reyes, G.E., Doctrines in categorical logic, () · Zbl 0359.14015
[16] Lafont, Y., The linear abstract machine, Theoret. comput. sci., 59, (1988) · Zbl 0648.68016
[17] Lambek, J.; Scott, P.J., Introduction to higher-order categorical logic, () · Zbl 0642.03002
[18] MacLane, S., ()
[19] Manes, E., Algebraic theories, () · Zbl 0353.18007
[20] Mason, I.A., Verification of programs that destructively manipulate data, Sci. comput. programming, 10, (1988) · Zbl 0647.68020
[21] Moggi, E., Categories of partial morphisms and the partial lambda-calculus, () · Zbl 0628.03007
[22] Moggi, E., The partial lambda-calculus, () · Zbl 0599.03051
[23] Moggi, E., (), Lecture Notes for course CS 359, Stanford Univ.
[24] Moggi, E., A category-theoretic account of program modules, () · Zbl 0747.18009
[25] Moggi, E., Computational lambda-calculus and monads, () · Zbl 0716.03007
[26] Mosses, P., (), [To appear in Handbook of Theoretical Computer Science, North-Holland, Amsterdam]
[27] Makkai, M.; Reyes, G., ()
[28] Mason, I.; Talcott, C., Programming, transforming, and proving with function abstractions and memories, ()
[29] Mason, I.; Talcott, C., A sound and complete axiomatization of operational equivalence of programs with memory, ()
[30] Plotkin, G.D., Call-by-name, call-by-value and the λ-calculus, Theoret. comput. sci., 1, (1975) · Zbl 0325.68006
[31] Plotkin, G.D., Denotational semantics with partial functions, () · Zbl 0512.68012
[32] Rosolini, G., Continuity and effectiveness in topoi, ()
[33] Schmidt, D.A., ()
[34] Scott, D.S., A type-theoretic alternative to CUCH, ISWIM, OWHY, Oxford notes, (1969)
[35] Scott, D.S., Identity and existence in intuitionistic logic, () · Zbl 0418.03016
[36] Scott, D.S., Recating theories of the λ-calculus, ()
[37] Seely, R.A.G., Linear logic, ∗-autonomous categories and cofree coalgebras, () · Zbl 0674.03007
[38] Sharma, K., Syntactic aspects of the non-deterministic lambda calculus, (), [Available as Internal Report CS-84-127 of the Computer Science Department]
[39] Smith, M.; Plotkin, G., The category-theoretic solution of recursive domain equations, SIAM J. comput., 11, (1982) · Zbl 0493.68022
[40] Street, R., The formal theory of monads, J. pure appl. algebra, 2, (1972) · Zbl 0241.18003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.