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

Revista:
Lecture Notes on Software Engineering

ISSN: 2301-3559

Año de publicación: 2014

Volumen: 2

Número: 4

Páginas: 288-293

Tipo: Artículo

DOI: 10.7763/LNSE.2014.V2.138 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Lecture Notes on Software Engineering

Resumen

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.

€ Ver financiación

Información de financiación

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.

Financiadores

Referencias bibliográficas

  • 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.