Abstract
In this paper, we describe a computer system CAL which assists studentsé understanding of a lecture course in logic and computation. We introduce a new foundational theory of expressions, which is inspired by the theory of expressions due to Martin-Löf [6], and use the expressions determined by the theory to implement various syntactic objects in CAL. We also introduce the concept of derivation game, and show that various logical and computational systems given in the lecture course can be defined uniformly by derivation games.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, North-Holland, 1981.
Barwise, J. and J. Etchemendy, Tarski’s World, CSLI Lecture Notes, No. 25, CSLI Publications, Cambridge University Press, 1994.
de Bruijn, D. G., Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, Indag. Math. 34, pp. 381–392, 1972.
Harper, R., F. Honsell, and G. Plotkin, A Framework for Defining Logics, Journal of the Association for Computing Machinery, Vol. 40, No. 1, pp. 143–184, 1993.
Huet, G., and G. Plotkin eds., Logical Frameworks, Cambridge University Press, 1991.
Nordström, B., K. Petersson, and J. M. Smith, Programming in Martin-Löf’ s Type Theory, Oxford University Press, 200 pages, 1990.
Sato, M., and M. Hagiya, Hyperlisp, in de Bakker, van Vliet eds., Algorithmic Languages, North-Holland, pp. 251–269, 1981.
Sato, M., Theory of Symbolic Expressions, II, Publ. of Res. Inst. for Math. Sci., Kyoto Univ., 21, pp. 455–540, 1985.
Sato, M., An Abstraction Mechanism for Symbolic Expressions, in V. Lifschitz ed., Artificial Intelligence and Mathematical Theory of Computation (Papers in Honor of John McCarthy), Academic Press, pp. 381–391, 1991.
Sato, M., T. Sakurai and R. Burstall, Explicit Environments, Fundamenta Informaticae 45, pp. 79–115, 2001.
Sato, M., T. Sakurai and Y. Kameyama, A Simply Typed Context Calculus with First-Class Environments, Proc. Fifth International Symposium on Functional and Logic Programming (FLOPS), Lecture Notes in Computer Science 2024, pp. 359–374, 2001.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sato, M., Kameyama, Y., Izumi, T. (2001). CAL: A Computer Assisted Learning System for Computation and Logic. In: Moreno-Díaz, R., Buchberger, B., Luis Freire, J. (eds) Computer Aided Systems Theory — EUROCAST 2001. EUROCAST 2001. Lecture Notes in Computer Science, vol 2178. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45654-6_40
Download citation
DOI: https://doi.org/10.1007/3-540-45654-6_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42959-3
Online ISBN: 978-3-540-45654-4
eBook Packages: Springer Book Archive