Electrical computers and digital processing systems: memory – Storage accessing and control – Memory configuring
Reexamination Certificate
2011-07-05
2011-07-05
Nguyen, Hiep T (Department: 2187)
Electrical computers and digital processing systems: memory
Storage accessing and control
Memory configuring
Reexamination Certificate
active
07975121
ABSTRACT:
Embodiments that facilitate type checking of assembly language instructions are disclosed. In one embodiment, a method includes receiving a low level language instruction in a memory. The instruction includes a word having a first type. The memory includes either a stack or a heap. Each of the stack or heap includes a plurality of positions. The method also includes labeling the plurality of positions in one of the stack or the heap as one or more specified positions and one or more unspecified positions. The method further includes assigning a second type to the memory, the second type including the first type of the word. The word is stored in a specified position or an unspecified position. The method additionally includes determining whether the instruction is well-typed by applying one or more rules to the instruction and to the second type.
REFERENCES:
patent: 6072950 (2000-06-01), Steensgaard
patent: 7574700 (2009-08-01), Bracha
Ahmed et al., “The Logical Approach to Stack Typing”, ACM SIGPLAN Notices, vol. 38, Issue 3, Mar. 2003, 12 pgs.
Crary, “Toward a Foundational Typed Assembly Language”, ACM SIGPLAN Notices, vol. 38, Issue 1, Jan. 2003, 15 pgs.
Crary et al., “Typed Memory Management in a Calculus of Capabilities”, Proceedings of 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, 1999, 14 pgs.
Fluet et al., “Linear Regions Are All You Need”, Lecture Notes in Computer Science (LNCS), Programming Languages and Systems, vol. 3924, 2006, 15 pgs.
Girard, “Linear Logic”, Theoretical Computer Science, vol. 50, Issue 1, Jan. 1987, 102 pgs.
Ishtiaq et al., “BI as an Assertion Language for Mutable Data Structures”, Proceedings 28th ACM-SIGPLAN Symposium on Principles of Programming Lanaguage, Jan. 2001, 13 pgs.
Jia et al., “Certifying Compilation for a Language with Stack Allocation”, 20th Annual IEEE Symposium on Logic in Computer Science, 2005, 10 pgs.
Lincoln et al., “Decision Problems for Propositional Linear Logic”, 31st Annual Symposium on Foundations of Computer Science, 1990, 10 pgs.
Morrisett et al., “From System F to Typed Assembly Language”, ACM Transactions on Programming Languages and Systems, vol. 21, Issue 3, May 1999, 41 pgs.
Morrisett et al., “Stack-Based Typed Assembly Language”, Journal of Functional Programming, 2002, vol. 12, 23 pgs.
Necula, “Proof-Carrying Code”, ACM Symposium on Principles of Programming Languages, 1997, 14 pgs.
Reynolds, “Separation Logic: A Logic for Shared Mutable Data Structures”, 17th Annual IEEE Symposium on Logic in Computer Science, 2002, 20 pgs.
Smith et al., “Alias Types”, Lecture Notes in Computer Science (LNCS), Programming Languages and Systems, vol. 1782, 2000, 16 pgs.
Wadler, “A Taste of Linear Logic”, Lecture Notes in Computer Science, Mathematical Foundations of Computers, vol. 711/1993, 21 pgs.
Walker, “Mechanical Reasoning about Low-Level Programming Languages”, Lecture Notes, 2001, retrieved from http://www.cs.cmu.edu/dpw/papers.html, 50 pgs.
Chen Juan
Hawblitzel Chris
Perry Frances
Lee & Hayes PLLC
Microsoft Corporation
Nguyen Hiep T
LandOfFree
Simple stack types does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Simple stack types, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Simple stack types will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2633795