Toward a foundational typed assembly language

ABSTRACT

We present the design of a typed assembly language called TALT that supports heterogeneous tuples, disjoint sums, and a general account of addressing modes. TALT also implements the von Neumann model in which programs are stored in memory, and supports relative addressing. Type safety for execution and for garbage collection are shown by machine-checkable proofs. TALT is the first formalized typed assembly language to provide any of these features.

REFERENCES

• 1: Andrew W. Appel , Amy P. Felty, A semantic model of types and machine instructions for proof-carrying code, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.243-253, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325727]
• 2: Hans-J. Boehm, Simple garbage-collector-safety, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.89-98, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 3: Hans-J. Boehm and David Chase. A proposal for garbage-collector-safe C compilation. The Journal of C Language Translation, 4(2):126--141, December 1992.
• 4: Hans-Juergen Boehm , Mark Weiser, Garbage collection in an uncooperative environment, Software—Practice & Experience, v.18 n.9, p.807-820, September 1988 [doi>10.1002/spe.4380180902]
• 5: Proceedings of the First IEEE/ACM International Workshop on Grid Computing, December 2000
• 6: Henry Cejtin , Suresh Jagannathan , Stephen Weeks, Flow-Directed Closure Conversion for Typed Languages, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.56-71, April 02, 2000
• 7: Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning. Trustless grid computing in ConCert. Technical Report CMU-CS-02-152, Carnegie Mellon University, School of Computer Science, June 2002.
• 8: Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.95-107, June 18-21, 2000, Vancouver, British Columbia, Canada
• 9: ConCert. http://www.cs.cmu.edu/char"7Econcert, September 2001.
• 10: Karl Crary. Toward a foundational typed assembly language. Technical Report CMU-CS-02-196, Carnegie Mellon University, School of Computer Science, December 2002.
• 11: Karl Crary , J. Gregory Morrisett, Type Structure for Low-Level Programming Languages, Proceedings of the 26th International Colloquium on Automata, Languages and Programming, p.40-54, July 11-15, 1999
• 12: Joshua Dunfield. Personal communication.
• 13: Nadeem A. Hamid , Zhong Shao , Valery Trifonov , Stefan Monnier , Zhaozhong Ni, A Syntactic Approach to Foundational Proof-Carrying Code, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.89-100, July 22-25, 2002
• 14: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 15: Intel Corporation. IA-32 Intel Architecture Software Developer's Manual, 2001. Order numbers 245470--245472.
• 16: Craig Lee, editor. Second International Workshop on Grid Computing, volume 2242 of Lecture Notes in Computer Science, Denver, Colorado, November 2001. Springer-Verlag.
• 17: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 18: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support for System Software, Atlanta, May 1999.
• 19: J. Gregory Morrisett , Karl Crary , Neal Glew , David Walker, Stack-Based Typed Assembly Language, Proceedings of the Second International Workshop on Types in Compilation, p.28-52, March 25-27, 1998
• 20: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 21: George C. Necula , S. P. Rahul, Oracle-based checking of untrusted software, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-154, January 2001, London, United Kingdom
• 22: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 23: Frank Pfenning , Ekkehard Rohwedder, Implementing the Meta-Theory of Deductive Systems, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.537-551, June 15-18, 1992
• 24: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 25: Frank Pfenning and Carsten Schürmann. Twelf User's Guide, Version 1.3R4, 2002. Available electronically at http://www.cs.cmu.edu/char"7Etwelf.
• 26: Ekkehard Rohwedder , Frank Pfenning, Mode and Termination Checking for Higher-Order Logic Programs, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.296-310, April 22-24, 1996
• 27: Carsten Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, October 2000.
• 28: SETI@Home. http://setiathome.ssl.berkeley.edu, November 2000.
• 29: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 30: Andrew Tolmach , Dino P. Oliva, From ML to Ada: Strongly-typed language interoperability via source translation, Journal of Functional Programming, v.8 n.4, p.367-412, July 1998 [doi>10.1017/S0956796898003086]
• 31: J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1--3):111--156, 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Security, Verification

Keywords:
proof-carrying code, typed assembly language