J. Zucker: Areas of Interest


1. Logic and Foundations; Proof theory; Automatic proof checking

My background is in mathematical logic and the foundations of mathematics, particularly proof theory. I obtained my PhD in Mathematics in this area, at Stanford University under Prof. S. Feferman in 1971. [1] is based on my thesis. [4] is an application of foundational work to automatic proof checking. [5] and [6] have philosophical aspects. Interestingly, some of my recent work in computability theory ([18] in Section 4 below) make extensive use of proof theory. [7] and [8] are expository.

Some publications in this area:

  1. J.I. Zucker (1973): Iterated inductive definitions, trees and ordinals. Chapter 6 of Mathematical Investigation of Intuitionistic Arithmetic and Analysis, ed. A.S. Troelstra, Lecture Notes in Mathematics, 344 (Springer-Verlag). Second corrected edition (Institute for Logic, Language and Computation, University of Amsterdam, 1993), 392-453.
  2. J.I. Zucker (1974): The correspondence between cut-elimination and normalization. Part I. Intuitionistic predicate logic, Annals of Mathematical Logic, 7, 1-112.
  3. J.I. Zucker (1974): The correspondence between cut-elimination and normalization. Part II. Heyting's arithmetic, Annals of Mathematical Logic, 7, 113-155.
  4. J.I. Zucker (1977): Formalization of classical mathematics in AUTOMATH, Clermont-Ferrand, France, July 1975, Colloques Internationaux du Centre National de la Recherche Scientifique, No. 249 (Centre National de la Recherche Scientifique, Paris). Reprinted in Selected Papers in Automath, ed. R.P. Nederpelt and H. Geuvers (North-Holland, 1994), 127-139.
  5. J.I. Zucker and R.S. Tragesser (1978): The adequacy problem for inferential logic, Journal of Philosophical Logic, 7, 501-516.
  6. J.I. Zucker (1978): The adequacy problem for classical logic, Journal of Philosophical Logic, 7, 517-535.
  7. J.I. Zucker (1993): Propositional temporal logics and their use in model checking, in Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, ed. P.E. Lauer, Lecture Notes in Computer Science 693 (Springer-Verlag), 108-116. [abstract, text.ps.gz].
  8. J.I. Zucker (1993): The propositional mu-calculus and its use in model checking, in Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University. [abstract, text.ps.gz].



2. Semantics of Programming Languages

I have worked in program semantics, especially denotational semantics, collaborating with Jaco de Bakker and his colleagues at the CWI (Centre for Mathematics and Computer Science, formerly Mathematical Centre), Amsterdam. Most of the papers below result from this collaboration.

I have also worked on applications of intensional logic to program semantics [4] collaborating with H.K. Hung, as a development of his doctoral thesis under my direction (1990), and, more recently, with Marc Bender as a development of his thesis [7].

Some publications in this area:

  1. J.W. de Bakker and J.I. Zucker (1982): Processes and the denotational semantics of concurrency, Information and Control, 54, 70-120. Reprinted, with errata, in Studies in Concurrency Semantics: Selected Papers of the Amsterdam Concurrency Group, ed. J.W. de Bakker and J.J.M.M. Rutten (World Scientific Publ. Co., 1992), 28-80.
  2. J.W. de Bakker, J.-J. Ch. Meyer and J.I. Zucker (1983): On infinite computations in denotational semantics, Theoretical Computer Science, 26, 53-82. Contrasting themes in the semantics of imperative concurrency, Current Trends in Concurrency (Overviews and Tutorials): , 224 (Springer-Verlag), 51-121.
  3. J.W. de Bakker, J.-J. Ch. Meyer, E.R. Olderog and J.I. Zucker (1988): Transition systems, metric spaces, and ready sets in the semantics of uniform concurrency, Journal of Computer and System Sciences, 54, 158-224.
  4. H.K. Hung and J.I. Zucker (1991): Semantics of pointers, referencing and dereferencing with intensional logic, in Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, July 1991, 127-136. [abstract, text.pdf] Program semantics, intensional logic and compositionality, in Proceedings of the First Montreal Workshop on , abstract, text.ps.gz]
  5. J.I. Zucker and J.J.M.M. Rutten (1992): A semantic approach to fairness, Fundamenta Informaticae 16, 1-38.
  6. P. Wegner and J.I. Zucker (1993): Article on Programming language semantics, in Encyclopedia of Computer Science and Engineering, 3rd edition, ed. A. Ralston and E.D. Reilly (Van Nostrand Reinhold), 1115-1118.
  7. Marc Bender and Jeffery Zucker (2013): Assignment calculus: A pure imperative language, Symposium on Logical Foundations of Computer Science, San Diego, Jan. 2013, ed. S. Artemov and A. Nerode. Lecture Notes in Computer Science 7734, Springer-Verlag. [preprint.pdf]



3. Logical foundations of software documentation

I have collaborated with D.L. Parnas and his colleagues and students in the Software Quality Research Laboratory in the Department of Computing & Software, in the area of formal descriptions of software. More specifically, I have worked on the theory of tabular notations developed by Parnas, which are of great use in such descriptions, notably for safety-critical software.

Some publications in this area:

  1. H. Shen, J.I. Zucker, D.L. Parnas (1996): Table transformation tools: Why and how. in COMPASS '96: Proceedings of the Eleventh Annual Conference on Computer Assurance, Gaithersburg, Maryland, USA, June 1996 (IEEE and National Institute of Standards and Technology), 3-11. [abstract, text.ps.gz]
  2. J.I. Zucker (1996): Transformations of normal and inverted function tables, Formal Aspects of Computing 8, 679-705. [abstract, text.ps.gz]
  3. R. Janicki, D.L. Parnas, J. Zucker (1997): Tabular representations in relational documents, in Relational Methods in Computer Science, ed. C. Brink, W. Kahl and G. Schmidt (Springer-Verlag), 184-196. [abstract, text.ps.gz]
  4. J.I. Zucker and H. Shen (1998): Table transformation: Theory and tools, McMaster University, Dept of Computing and Software, Report CAS 98-01; also Communications Research Laboratory (CRL) Report 363. [abstract, text.ps.gz, tables.ps.gz ( Note: the file "tables.ps" contains two tables to be inserted between pages 4 and 5 of the text.)]



4. Computability on abstract and topological algebras; Analog computing

This is an ongoing research project, in collaboration with J.V. Tucker of University of Wales Swansea. Our collaboration began with our book [1], and is still very active. Interestingly, some of our recent work [18] make extensive use of proof theory (see Section 1 above). Paper [5] is an exposition of the classical theory, and provides a useful background for the other papers. Publication [8] is a detailed exposition of much of our prior work. Paper [7], and most of the publications from [9] on (except for [13] and [18]) represent the current focus of our attention in this field, namely computation on topological algebras and stream algebras, and, more specifically, the reals. Two themes, in particular, are emphasised in this more recent work: (a) the relationship between abstract and concrete models of computation on metric partial algebras such as the reals [11, 12, 15, 16], and (b) the relationship between digital and analog (or "unconventional") computation [14, 17, 19] (where [17] is a detailed exposition of [14]). Paper [13] is based on Jian Xu's MSc Thesis, completed August 2003. Paper [18] is a generalisation to abstract many-sorted algebras of a classical proof-theoretic result of Parsons, Mints and Takeuti. Paper [21] is based on Chapter 3 of Nick James's PhD Thesis, completed August 2012.

Some publications in this area:

  1. J.V. Tucker and J.I. Zucker (1988): Program Correctness over Abstract Data Types, with Error-State Semantics (North-Holland).
  2. J.V. Tucker and J.I. Zucker (1991): Projections of semicomputable relations on abstract data types. International Journal of Foundations of Computer Science, 2, 267-296. [abstract, text.ps.gz]
  3. J.V. Tucker and J.I. Zucker (1992): Examples of semicomputable sets of real and complex numbers, in Constructivity in Computer Science -- Proceedings of a Summer Symposium, San Antonio, Texas, June 1991, ed. J.P. Myers, Jr. and M.J. O'Donnell, Jr., Lecture Notes in Computer Science 613, (Springer-Verlag), 179-198. [abstract]
  4. J.V. Tucker and J.I. Zucker (1992): Deterministic and nondeterministic computation, and Horn programs, on abstract data types, Journal of Logic Programming 13, 23-55.
  5. L. Pretorius and J.I. Zucker (1993): Introduction to computability theory, South African Computer Journal, 9, April 1993, 3-30. [abstract, text.pdf]
  6. J.V. Tucker and J.I. Zucker (1994): Computable functions on stream algebras, in
    NATO Advanced Study Institute, International Summer School on Proof and Computation, Marktoberdorf, Germany, 1993, ed. H. Schwichtenberg (Springer-Verlag), 341-382. [abstract, text.ps.gz].
  7. J.V. Tucker and J.I. Zucker (1999): Computation by 'While' programs on topological partial algebras, Theoretical Computer Science 219, 379--420. [abstract, PDF via ScienceDirect]
  8. J.V. Tucker and J.I. Zucker (2000): Computable functions and semicomputable sets on many-sorted algebras, in "Handbook of Logic in Computer Science", Vol. 5, ed. S. Abramsky, D.M. Gabbay and T.S.E. Maibaum (Oxford University Press), 317-523. [abstract, PDF]
  9. J.V. Tucker and J.I. Zucker (2002): Infinite initial algebra specifications for stream algebras, in "Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman", ed. W. Sieg, R. Sommer and C. Talcott, Lecture Notes in Logic, vol. 15, 234--256. (Association for Symbolic Logic). [abstract, text.ps.gz]
  10. J.V. Tucker and J.I. Zucker (2002): Abstract computability and algebraic specification, ACM Transactions on Computational Logic, 3, 279-333. [abstract, preprint.pdf, PDF via ACM Portal]
  11. J.V. Tucker and J.I. Zucker (2004): Abstract versus Concrete Computation on Metric Partial Algebras. ACM Transactions on Computational Logic 5, 611-668. [abstract, preprint.pdf, PDF via ACM Portal,appendix.pdf]
  12. J.V. Tucker and J.I. Zucker (2005): Computable total functions, algebraic specifications and dynamical systems. Journal of Logical and Algebraic Programming, 62, 71-108. [abstract, preprint.pdf, PDF via ScienceDirect]
  13. J. Xu and J.I. Zucker (2005): First and second order recursion on abstract data types. Fundamanta Informaticae, 67, 377-419. [abstract, preprint.pdf, PDF via IOS Press (Search with terms "fundamenta xu zucker")]
  14. J.V. Tucker and J.I. Zucker (2005): A Network Model of Analogue Computation over Metric Algebras. New Computational Paradigms: First Conference on Computability in Europe, CiE 2005, Amsterdam, June 2005: Proceedings, ed. S.B. Cooper, B. Löwe, and L. Torenvliet. Lecture Notes in Computer Science 3526, Springer-Verlag, 515-529. [abstract, preprint.pdf, PDF via SpringerLink]
  15. J.V. Tucker and J.I. Zucker (2006): Abstract versus concrete computability: The case of countable algebras. Logic Colloquium '03, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Helsinki, August 2003, ed. V. Stoltenberg-Hansen and J. Väänänen. Lecture Notes in Logic 24, Association for Symbolic Logic and A.K. Peters, 377-408. [abstract, preprint.pdf]
  16. W. Jiang, Y. Wang and J.I. Zucker (2007): Universality and Semicomputability for Nondeterministic Programming Languages over Abstract Algebras. Journal of Logic and Algebraic Programming, 71, 44-78. (Based on Wei Jiang's and Yuan Wang's MSc Theses, 2002 and 2001.) [preprint.pdf, PDF via ScienceDirect]
  17. J.V. Tucker and J.I. Zucker (2007): Computability of analog networks. Theoretical Computer Science, 371, 115-146. [abstract, preprint.pdf, PDF via ScienceDirect]
  18. T. Strahm and J.I. Zucker (2008): Primitive recursive selection functions for existential assertions over abstract algebras. Journal of Logic and Algebraic Programming, (Special Issue on Logic and Information: From Logic to Constructive Reasoning, ed. V. Brattka, G. Jaeger, H.P. Kuenzi), 76, 175-197. [preprint.pdf, PDF via ScienceDirect]
  19. B.C. Thompson, J.V. Tucker and J.I. Zucker (2009): Unifying computers and dynamical systems using the theory of synchronous concurrent algorithms. Applied Mathematics and Computation (Special Issue on Physics and Computation, ed. C. Calude and J.F. Costa), 215, 1386-1403. [preprint.pdf, PDF via ScienceDirect]
  20. J.V. Tucker and J.I. Zucker (2011): Continuity of operators on continuous and discrete time streams. Theoretical Computer Science, 412, 3378-3403. [preprint.pdf, PDF via ScienceDirect]
  21. Nick D. James and Jeffery Zucker (2013): A class of contracting stream operators. The Computer Journal, 56, 15-33. Abstract, Reprint.
  22. J.V. Tucker and J.I. Zucker (2014): Computability of operators on continuous and discrete time streams. Computability, 3, 9-44. [PDF]
  23. Bo Xie, Ming Quan Fu and Jeffery Zucker (2015): Characterizations of Semicomputable Sets of Real Numbers, Journal of Logical and Algebraic Methods in Programming, 84, 124-154. [preprint.pdf, article.pdf]
  24. Ming Quan Fu and Jeffery Zucker (2015): Models of Computation for Partial Functions on the Reals, Journal of Logical and Algebraic Methods in Programming, 84, 218-237. [preprint.pdf, article.pdf]
  25. J.V. Tucker and J.I. Zucker (2015): Generalizing computability theory to abstract algebras, in "Turing's Revolution. The Impact of his Ideas about Computability", ed. G. Sommaruga and T. Strahm (Birkhauser/Springer Basel), 127-1604. [preprint.pdf]



    Last revised March 11, 2015 (Please inform me of any bad links.)
    zucker@mcmaster.ca