Automatic Generation of Object-Oriented Type Checkers

  1. Ortin, Francisco 1
  2. Zapico, Daniel 1
  3. Quiroga, Jose 1
  4. Garcia, Miguel 1
  1. 1 Universidad de Oviedo
    info

    Universidad de Oviedo

    Oviedo, España

    ROR https://ror.org/006gksa02

Aldizkaria:
Lecture Notes on Software Engineering

ISSN: 2301-3559

Argitalpen urtea: 2014

Alea: 2

Zenbakia: 4

Orrialdeak: 288-293

Mota: Artikulua

DOI: 10.7763/LNSE.2014.V2.138 GOOGLE SCHOLAR lock_openSarbide irekia editor

Beste argitalpen batzuk: Lecture Notes on Software Engineering

Laburpena

Type systems are aimed at preventing programming language constructions from having wrong behavior at runtime. Different formalisms are used to guarantee that a type system is well defined. However, the type systems implemented in commercial language processors (type checkers) do not commonly use tools that translate these formalisms into code. We propose a framework to facilitate the implementation of object-oriented type checkers, following widespread design patterns. A tool generates the specific implementation of a type checker, receiving a specification of the type system as its input. The generated code interacts with an API, accessible from the rest of the language processor implementation.

Finantzaketari buruzko informazioa

This work was partially funded by the Department of Science and Innovation (Spain) under the National Program for Research, Development and Innovation: project TIN2011-25978, entitled Obtaining Adaptable, Robust and Efficient Software by Including Structural Reflection in Statically Typed Programming Languages.

Finantzatzaile

Erreferentzia bibliografikoak

  • A. N. Whitehead and B. Russell, Principia Mathematica, Cambridge University Press, 1910.
  • B. C. Pierce. Types and Programming Languages, MIT Press, 2002.
  • L. Cardelli, “Type systems,” The Computer Science and Engineering Handbook, CRC Press, 2004.
  • A. V. Aho, J. D. Ullman, and R. Sethi, Compilers: Principles, Techniques, and Tools, Addison Wesley, 1985.
  • F. Ortin, M. A. Labrador, and J. M. Redondo, “A hybrid class- and prototype-based object model to support language-neutral structural intercession,” Information and Software Technology, vol. 56, no. 2, pp. 199-219, February 2014.
  • J. M. Redondo, F. Ortin, and J. M. Cueva, “Optimizing reflective primitives of dynamic languages,” International Journal of Software Engineering and Knowledge Engineering, vol. 18, no. 6, pp. 759-783, September 2008.
  • A. K. Wright and M. Felleisen, “A syntactic approach to type soundness,” Information and Computation, vol. 115, no. 1, pp. 38-94, November 1994.
  • C. Grothoff, J. Palsberg, and J. Vitek, “Encapsulating objects with confined types,” ACM Transactions on Programming Languages and Systems, vol. 29, no. 6, October 2007.
  • D. J. Richardson, “TAOS: Testing with analysis and Oracle support,” in Proc. International Symposium on Software Testing and Analysis, August 1994, pp. 138-153.
  • H. Hosoya and B. C. Pierce, “XDuce: A statically typed XML processing language,” ACM Transactions on Internet Technology, vol. 3, no. 2, pp. 117-148, May 2003.
  • M. Abadi, “Security Protocols and Specifications,” Foundations of Software Science and Computation Structures (FOSSACS), Lecture Notes in Computer Science, vol. 1578, pp. 1-13, March 1999.
  • F. P. Ramsey, “The foundations of mathematics,” in Proc. the London Mathematical Society, vol. 25, 1925.
  • A. Church, “A formulation of the simple theory of types,” Journal of Symbolic Verification and Synthesis, vol. 5, no. 2, pp. 56-68, June 1940.
  • P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984.
  • S. Berardi, “Towards a mathematical analysis of the Coquand-Huet Calculus of Constructions and the other systems in Barendregt’s cube,” Technical report, Department of Computer Science, Carnegie-Mellon University, 1988.
  • D. E. Knuth, “Semantics of context-free languages,” Mathematical Systems Theory, vol. 2, no. 2, pp. 127-145, 1968.
  • T. Nipkow. (December 2013). Programming and Proving in Isabelle/HOL. [Online] Available: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/do c/prog-prove.pdf
  • A. Chlipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, The MIT Press, November 2013.
  • K. Rustan, M. Leino, G. Nelson, and J. B. Saxe, ESC/Java User's Manual, Compaq Systems Research Center, 2000.
  • T. Ball, and S. K. Rajamani, “The SLAM Project: Debugging System Software via Static Analysis,” Principles of Programming Languages (POPL), pp. 1-3, January 2002.
  • G. J. Holzmann, The Spin Model Checker, Addison Wesley, 2003.
  • M. Felleisen, R. B. Findler, and M. Flatt, Semantics Engineering with PLT Redex, The MIT Press, August 2009.
  • T. W. Reps and T. Teitelbaum, “The synthesizer generator,” Software Engineering Symposium on Practical Software Development Environments (SDE), pp. 42-48, May 1984.
  • M. Brand et al., “The ASF+SDF Meta-environment: A Component-Based language development environment,” in Proc. Compiler Construction (CC), European Joint Conference on Theory and Practice of Software (ETAPS), April 2001, pp. 365-370.
  • H. Gast, “A generator for type checkers,” Ph.D. Thesis, Eberhard-Karls-Universit at Tübingen, 2004.
  • M. Y. Levin and B. C. Pierce, “TinkerType: A language for playing with formal systems,” Journal of Functional Programming, vol. 13, no. 2, pp. 295-316, March 2003.
  • M. L. Scott, Programming Language Pragmatics, Morgan Kaufmann Publishers, 2000.
  • F. Ortin, J. M. Cueva, and D. Zapico, “Patterns for teaching type checking in a compiler construction course,” IEEE Transactions on Education, vol. 50, no. 3, pp. 273-283, August 2007.
  • T. Parr, The Definitive ANTLR 4 Reference, 2nd ed., Pragmatic Bookshelf, January 2013.
  • F. Ortin and D. Zapico. (December 2013). A Framework to Facilitate the Development of Object-Oriented Type Checkers. TyS. [Online]. Available: http://www.reflection.uniovi.es/tys
  • E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns: Elements of Reusable Object-Oriented Software, Addison Wesley, October 1994. D. Zapico, “Design and implementation of a tool for the automatic generation of object-oriented type systems,” Master Thesis, Polytechnic School of Engineering, University of Oviedo, March 2003.
  • M. Grand, Patterns in Java, A Catalog of Reusable Design Patterns Illustrated With UML, vol. I, Wiley, 1999.
  • F. Ortin, B. Lopez, and J. B. G. Perez-Schofield, “Separating adaptable persistence attributes through computational reflection,” IEEE Software, vol. 21, no. 6, pp. 41-49, November 2004.
  • F. Ortin and D. Diez, “Designing an adaptable heterogeneous abstract machine by means of reflection,” Information and Software Technology, vol. 47, no. 2, pp. 81-94, February 2005.
  • F. Ortin, D. Zapico, J. B. B. Perez-Schofield, and M. Garcia, “Including both static and dynamic typing in the same programming language,” IET Software, vol. 4, no. 4, pp. 268-282, August 2010.
  • F. Ortin and M. Garcia, “Union and intersection types to support both dynamic and static typing,” Information Processing Letters, vol. 111, no. 6, pp. 278-286, February 2011.