research-article

Open access

Semantic foundations for typed assembly languages

Authors:

Amal Ahmed,

Andrew W. Appel,

Christopher D. Richards,

Kedar N. Swadi,

Gang Tan,

Daniel C. WangAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 32, Issue 3

Article No.: 7, Pages 1 - 67

https://doi.org/10.1145/1709093.1709094

Published: 16 March 2010 Publication History

PDF eReader

Abstract

Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and L_c, a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and L_c to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler.

To prove the soundness of the TML type system we have successfully applied a new approach, that of step-indexed logical relations. This approach provides the first semantic model for a type system with updatable references to values of impredicative quantified types. Both impredicative polymorphism and mutable references are essential when representing function closures in compilers with typed closure conversion, or when compiling objects to simpler typed primitives.

References

[1]

Abadi, M. and Cardelli, L. 1996. A Theory of Objects. Springer, New York.

Digital Library

Google Scholar

[2]

Abramsky, S., Honda, K., and McCusker, G. 1998. A fully abstract game semantics for general references. In Proceedings of the 13th IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 334--344.

Digital Library

Google Scholar

[3]

Acar, U., Ahmed, A., and Blume, M. 2008. Imperative self-adjusting computation. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 309--322.

Digital Library

Google Scholar

[4]

Ahmed, A. 2006. Step-Indexed syntactic logical relations for recursive and quantified types. In Proceedings of the 15th European Symposium on Programming (ESOP). Springer, 69--83.

Digital Library

Google Scholar

[5]

Ahmed, A., Appel, A. W., and Virga, R. 2002. A stratified semantics of general references embeddable in higher-order logic. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos, CA, 75--86.

Digital Library

Google Scholar

[6]

Ahmed, A., Appel, A. W., and Virga, R. 2003. An indexed model of impredicative polymorphism and mutable references. http://www.cs.princeton.edu/~appel/papers/impred.pdf.

Google Scholar

[7]

Ahmed, A. and Blume, M. 2008. Typed closure conversion preserves observational equivalence. In Proceedings of the ACM International Conference on Functional programming (ICFP). ACM Press, New York, 157--168.

Digital Library

Google Scholar

[8]

Ahmed, A., Fluet, M., and Morrisett, G. 2005. A step-indexed model of substructural state. In Proceedings of the ACM International Conference on Functional programming (ICFP). ACM Press, New York, 78--91.

Digital Library

Google Scholar

[9]

Ahmed, A., Fluet, M., and Morrisett, G. 2007. L3: A linear language with locations. Fundam. Inf. 77, 4, 397--449.

Digital Library

Google Scholar

[10]

Ahmed, A. J. 2004. Semantics of types for mutable state. Ph.D. thesis, Princeton University, Princeton, New Jersey. Tech. rep. TR-713-04.

Digital Library

Google Scholar

[11]

Aiken, A., Foster, J. S., Kodumal, J., and Terauchi, T. 2003. Checking and inferring local non-aliasing. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI). ACM Press, New York.

Digital Library

Google Scholar

[12]

Appel, A. W. 1985. Semantics-directed code generation. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 315--324.

Digital Library

Google Scholar

[13]

Appel, A. W. 2000. Hints on proving theorems in Twelf. www.cs.princeton.edu/~appel/twelf-tutorial.

Google Scholar

[14]

Appel, A. W. 2001. Foundational proof-carrying code. In Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos, CA, 247--258.

Digital Library

Google Scholar

[15]

Appel, A. W. and Felty, A. P. 2000. A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 243--253.

Digital Library

Google Scholar

[16]

Appel, A. W. and MacQueen, D. B. 1991. Standard ML of New Jersey. In Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming, M. Wirsing, Ed. Springer, New York, 1--13.

Crossref

Google Scholar

[17]

Appel, A. W. and McAllester, D. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23, 5 657--683.

Digital Library

Google Scholar

[18]

Appel, A. W., Mellies, P.-A., Richards, C. D., and Vouillon, J. 2007. A very modal model of a modern, major, general type system. In Proceedings of the 34th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 109--122.

Digital Library

Google Scholar

[19]

Appel, A. W., Michael, N. G., Stump, A., and Virga, R. 2003. A trustworthy proof checker. J. Autom. Reas. 31, 231--260.

Digital Library

Google Scholar

[20]

Arbib, M. and Alagic, S. 1979. Proof rules for gotos. Acta Inf. 11, 139--148.

Digital Library

Google Scholar

[21]

Benton, N. 2005. A typed, compositional logic for a stack-based abstract machine. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science, vol. 3780. Springer, Berlin.

Digital Library

Google Scholar

[22]

Benton, N. 2006. Abstracting allocation: The new new thing. In Proceedings of the Computer Science Logic, 20th International Workshop (CSL'06). Lecture Notes in Computer Science, vol. 4207. Springer, Berlin.

Digital Library

Google Scholar

[23]

Benton, N. and Leperchey, B. 2005. Relational reasoning in a nominal semantics for storage. In Proceedings of the International Conference on Typed Lambda Calculi and Applications. Springer, Berlin, 86--101.

Digital Library

Google Scholar

[24]

Benton, N. and Zarfaty, U. 2007. Formalizing and verifying semantic type soundness for a simple compiler. In Proceedings of the 9th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP). ACM Press, New York.

Digital Library

Google Scholar

[25]

Birkedal, L. and Harper, R. 1997. Relational interpretations of recursive types in an operational setting. In Theoretical Aspects of Computer Software. Springer, Berlin.

Digital Library

Google Scholar

[26]

Bohr, N. and Birkedal, L. 2006. Relational reasoning for recursive types and references. In Proceedings of the 4th Asian Symposium on Programming Languages and Systems (APLAS). Springer, Berlin.

Digital Library

Google Scholar

[27]

Cardelli, L. 1997. Program fragments, linking, and modularization. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 266--277.

Digital Library

Google Scholar

[28]

Chen, J. 2004. A low-level typed assembly language with a machine-checkable soundness proof. Ph.D. thesis, Princeton University, Princeton, New Jersey. Tech. rep. CS-TR-704-04.

Digital Library

Google Scholar

[29]

Chen, J., Wu, D., Appel, A. W., and Fang, H. 2003. A provably sound TAL for back-end optimization. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI). ACM Press, New York, 208--219.

Digital Library

Google Scholar

[30]

Church, A. 1940. A formulation of the simple theory of types. J. Symb. Logic 5, 2, 56--68.

Crossref

Google Scholar

[31]

Clint, M. and Hoare, C. A. R. 1972. Program proving: Jumps and functions. Acta Informatica 1, 214--224.

Digital Library

Google Scholar

[32]

Colby, C., Lee, P., Necula, G. C., Blau, F., Cline, K., and Plesko, M. 2000. A certifying compiler for Java. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI). ACM Press, New York.

Digital Library

Google Scholar

[33]

Crary, K. 2000. Typed compilation of inclusive subtyping. In Proceedings of the ACM International Conference on Functional programming (ICFP). ACM Press, New York, 68--81.

Digital Library

Google Scholar

[34]

Crary, K. 2003. Toward a foundational typed assembly language. In Proceedings of the 30th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 198--212.

Digital Library

Google Scholar

[35]

Crary, K. and Harper, R. 2007. Syntactic logical relations for polymorphic and recursive types. Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin., Electtonic Notes in Theoretical Computer Science vol. 172, 259--299.

Digital Library

Google Scholar

[36]

Crary, K. and Sarkar, S. 2003. Foundational certified code in a metalogical framework. In Proceedings of the 19th International Conference on Automated Deduction (CADE'03). Springer, Berlin, 106--120.

Google Scholar

[37]

de Bruin, A. 1981. Goto statements: Semantics and deduction systems. Acta Informatica 15, 385--424.

Digital Library

Google Scholar

[38]

Feng, X., Ni, Z., Shao, Z., and Guo, Y. 2007. An open framework for foundational proof-carrying code. In Proceedings of the ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI). ACM Press, New York, 67--78.

Digital Library

Google Scholar

[39]

Girard, J.-Y. 1972. Interprétation fonctionnelle et elimination des coupures dans l'arithmétique d'ordre supérieur. Ph.D. thesis, University of Paris VII.

Google Scholar

[40]

Glew, N. and Morrisett, G. 1999. Type-Safe linking and modular assembly language. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 250--261.

Digital Library

Google Scholar

[41]

Hamid, N., Shao, Z., Trifonov, V., Monnier, S., and Ni, Z. 2002. A syntactic approach to foundational proof-carrying code. In Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, Los Alamitos, CA, 89--100.

Digital Library

Google Scholar

[42]

Harper, R. 1994. A simplified account of polymorphic references. Inf. Process. Lett. 51, 201--206.

Digital Library

Google Scholar

[43]

Harper, R. and Morrisett, G. 1995. Compiling polymorphism using intensional type analysis. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 130--141.

Digital Library

Google Scholar

[44]

Harper, R. and Pfenning, F. 2005. On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Logic 6, 1, 61--101.

Digital Library

Google Scholar

[45]

Hoare, C. A. R. 1969. An axiomatic basis for computer programming. Comm. ACM 12, 10, 578--580.

Digital Library

Google Scholar

[46]

Hriţcu, C. and Schwinghammer, J. 2008. A step-indexed semantics of imperative objects. In Informal Proceedings of the Workshop on Foundations of Object-Oriented Languages (FOOL).

Google Scholar

[47]

Kowaltowski, T. 1977. Axiomatic approach to side effects and general jumps. Acta Inf. 7, 4, 357--360.

Digital Library

Google Scholar

[48]

Levy, P. B. 2002. Possible world semantics for general storage in call-by-value. In Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic (CSL'02). Lecture Notes in Computer Science, vol. 2471. Springer, 232--246.

Digital Library

Google Scholar

[49]

MacQueen, D., Plotkin, G., and Sethi, R. 1986. An ideal model for recursive polymophic types. Inf. Comput. 71, 1/2, 95--130.

Digital Library

Google Scholar

[50]

Matthews, J. and Ahmed, A. 2008. Parametric polymorphiscm through run-time sealing, or, theorems for low, low prices. In Proceedings of the 17th European Symposium on Programming (ESOP). Springer, Berlin, 16--31.

Digital Library

Google Scholar

[51]

Melliès, P.-A. and Vouillon, J. 2004. Semantic types: A fresh look at the ideal model for types. In Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 52--63.

Digital Library

Google Scholar

[52]

Michael, N. G. and Appel, A. W. 2000. Machine instruction syntax and semantics in higher-order logic. In Proceedings of the 17th International Conference on Automated Deduction (CADE). Springer-Verlag, Berlin, 7--24. Lecture Notes in Artificial Intelligence, vol. 1831.

Digital Library

Google Scholar

[53]

Morrisett, G., Ahmed, A., and Fluet, M. 2005. L3: A linear language with locations. In Proceedings of the International Conference on Typed Lambda Calculi and Applications. Springer, Berlin, 293--307.

Digital Library

Google Scholar

[54]

Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., and Zdancewic, S. 1999a. TALx86: A realistic typed assembly language. In Proceedings of the 2nd ACM SIGPLAN Workshop on Compiler Support for System Software. ACM Press, New York, 25--35.

Google Scholar

[55]

Morrisett, G., Crary, K., Glew, N., and Walker, D. 2002. Stack-Based typed assembly language. J. Funct. Programm. 12, 1, 43--88.

Digital Library

Google Scholar

[56]

Morrisett, G., Walker, D., Crary, K., and Glew, N. 1998. From System F to typed assembly language. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 85--97.

Digital Library

Google Scholar

[57]

Morrisett, G., Walker, D., Crary, K., and Glew, N. 1999b. From System F to typed assembly language. ACM Trans. Programm. Lang. Syst. 21, 3, 527--568.

Digital Library

Google Scholar

[58]

Necula, G. C. 1997. Proof-Carrying code. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 106--119.

Digital Library

Google Scholar

[59]

Ni, Z. and Shao, Z. 2006. Certified assembly programming with embedded code pointers. In Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 320--333.

Digital Library

Google Scholar

[60]

O'Donnell, M. J. 1982. A critique of the foundations of Hoare style programming logics. Comm. ACM 25, 12, 927--935.

Digital Library

Google Scholar

[61]

Pfenning, F. and Schürmann, C. 1999. System description: Twelf—A meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE). Springer, Berlin.

Digital Library

Google Scholar

[62]

Pitts, A. M. 1996. Relational properties of domains. Inf. Comput. 127, 2, 66--90.

Crossref

Google Scholar

[63]

Pitts, A. M. 1998. Existential types: Logical relations and operational equivalence. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP'98). Lecture Notes Computer Science, vol. 1443. Springer, Berlin, 309--326.

Digital Library

Google Scholar

[64]

Pitts, A. M. 2000. Parametric polymorphism and operational equivalence. Math. Struc. Comput. Sci. 10, 321--359.

Digital Library

Google Scholar

[65]

Pitts, A. M. 2002. Operational semantics and program equivalence. In Applied Semantics, Advanced Lectures, G. Barthe, P. Dybjer, and J. Saraiva, Eds. Lecture Notes in Computer Science, vol. 2395. Springer, 378--412.

Digital Library

Google Scholar

[66]

Pitts, A. M. and Stark, I. D. B. 1993. Observable properties of higher order functions that dynamically create local names, or: What's new&quest; In Mathematical Foundations of Computer Science, A. M. Borzyszkowski and S. Sokolowski, Eds. Lecture Notes in Computer Science, vol. 711. Springer, Berlin, 122--141.

Digital Library

Google Scholar

[67]

Plotkin, G. D. 1973. Lambda-Definability and logical relations. Memo. SAI--RM--4, University of Edinburgh, Edinburgh, Scotland.

Google Scholar

[68]

Reynolds, J. C. 1981. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, Eds. North-Holland, Amsterdam, 345--372.

Google Scholar

[69]

Richards, C. D. 2009. The approximation modality in models of higher-order types. Ph.D. thesis, Princeton University, Princeton, New Jersey.

Google Scholar

[70]

Saabas, A. and Uustalu, T. 2005. A compositional natural semantics and Hoare logic for low-level languages. In Proceedings of the 2nd Workshop on Structured Operational Semantics (SOS'05).

Google Scholar

[71]

Scott, D. S. 1976. Data types as lattices. SIAM J. Comput. 5, 3, 522--587.

Digital Library

Google Scholar

[72]

Shao, Z. 1997. An overview of the FLINT/ML compiler. In Proceedings of the ACM SIGPLAN Workshop on Types in Compilation. ACM Press, New York.

Google Scholar

[73]

Stark, I. D. B. 1994. Names and higher-order functions. Ph.D. thesis, University of Cambridge, Cambridge, UK.

Google Scholar

[74]

Statman, R. 1985. Logical relations and the typed λ-calculus. Inf. Control 65, 2--3, 85--97.

Crossref

Google Scholar

[75]

Swadi, K. 2003. Typed machine language. Tech. rep. TR-676-03, Princeton University, Princeton, New Jersey.

Google Scholar

[76]

Tait, W. W. 1967. Intensional interpretations of functionals of finite type I. J. Symb. Logic 32, 2, 198--212.

Crossref

Google Scholar

[77]

Tan, G. 2005. A compositional logic for control flow and its application to foundational proof-carrying code. Tech. rep. CS-TR-731-05, Princeton University, Princeton, New Jersey.

Digital Library

Google Scholar

[78]

Tan, G. and Appel, A. W. 2006. A compositional logic for control flow. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 3855. Springer, Berlin, 80--94.

Digital Library

Google Scholar

[79]

Tan, G., Appel, A. W., Swadi, K. N., and Wu, D. 2004. Construction of a semantic model for a typed assembly language. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Compute Science, vol. 2937. Springer, Berlin, 30--43.

Google Scholar

[80]

Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., and Lee, P. 1996. TIL: A type-directed optimizing compiler for ML. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI). ACM Press, New York, 181--192.

Digital Library

Google Scholar

[81]

Wand, M. and Sullivan, G. T. 1997. Denotational semantics using an operationally-based term model. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, New York, 386--399.

Digital Library

Google Scholar

[82]

Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Inf. Comput. 115, 1, 38--94.

Digital Library

Google Scholar

[83]

Wu, D. 2005. Interfacing compilers, proof checkers, and proofs for foundational proof-carrying code. Tech. rep. CS-TR-733-05, Princeton University, Princeton, New Jersey.

Digital Library

Google Scholar

[84]

Wu, D., Appel, A. W., and Stump, A. 2003. Foundational proof checkers with small witnesses. In Proceedings of the 5th ACM International Conference on Principles and Practice of Declarative Programming (PADL). ACM Press, New York, 264--274.

Digital Library

Google Scholar

[85]

Yu, D., Hamid, N. A., and Shao, Z. 2003. Building certified libraries for PCC: Dynamic storage allocation. In Proceedings of the 12th European Symposium on Programming (ESOP). Springer.

Digital Library

Google Scholar

Cited By

View all

Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Patterson DWagner AAhmed ACong YDagand P(2023)Semantic Encapsulation using Linking TypesProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609405(14-28)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609405
Zhu FSammler MLepigre RDreyer DGarg D(2022)BFF: foundational and automated verification of bitfield-manipulating programsProceedings of the ACM on Programming Languages10.1145/35633456:OOPSLA2(1613-1638)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563345
Show More Cited By

Index Terms

Semantic foundations for typed assembly languages

Recommendations

Semantic analysis of normalisation by evaluation for typed lambda calculus
PPDP '02: Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming

This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can ...
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F

We formalize in the logical framework ATS/LF a proof based on Tait's method that establishes the simply-typed lambda-calculus being strongly normalizing. In this formalization, we employ higher-order abstract syntax to encode lambda-terms and an ...
Singleton: a general-purpose dependently-typed assembly language
TLDI '11: Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation

In this paper we present Singleton, a dependently typed assembly language. Based upon the calculus of inductive constructions, Singleton's type system allows procedures abstracting over terms, types, propositions, and proof terms.

Furthermore, Singleton ...

Reviews

Reviewer: Markus Wolf

A typed assembly language (TAL) is an assembly language that guarantees certain safety properties of a corresponding program, by virtue of type checking. In order to make this idea work for industry-strength assembly languages, a soundness proof for the corresponding TAL has to be developed, which is not a trivial endeavor. The goal of the project reported in this paper is to construct a machine-checked modular soundness proof for a realistic TAL. The paper describes an intermediate layer that consists of two key components. The first, typed machine language (TML), can be seen as a type theory geared toward describing properties of data and machine states. The second, L C , is a control logic based on "a generalized Hoare logic of multiple-entry and multiple-exit program[s]." These two components, including their syntax and semantics, and various other important properties are the focus of the first part of the paper. The second part of the paper shows how this intermediate layer is used to prove several soundness properties of a list manipulating an example TAL. Furthermore, it gives an overview of the Foundational Proof-Carrying Code (FPCC) project at Princeton, which consists of a complete machine-supported environment for the soundness proof of a richer TAL. The paper ends with a discussion of related work and a conclusion. This paper gives a very round and complete view of the conceptual and technical difficulties in designing a TAL and proving its soundness. It also provides some interesting insights into semantic modeling from real programming languages in a formal setting. In summary, this review cannot adequately express the paper's richness and complexity. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 32, Issue 3

March 2010

176 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1709093

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 March 2010

Accepted: 01 June 2009

Revised: 01 June 2009

Received: 01 November 2006

Published in TOPLAS Volume 32, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
1,105
Total Downloads

Downloads (Last 12 months)178
Downloads (Last 6 weeks)29

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Patterson DWagner AAhmed ACong YDagand P(2023)Semantic Encapsulation using Linking TypesProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609405(14-28)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609405
Zhu FSammler MLepigre RDreyer DGarg D(2022)BFF: foundational and automated verification of bitfield-manipulating programsProceedings of the ACM on Programming Languages10.1145/35633456:OOPSLA2(1613-1638)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563345
Spies SGäher LTassarotti JJung RKrebbers RBirkedal LDreyer D(2022)Later credits: resourceful reasoning for the later modalityProceedings of the ACM on Programming Languages10.1145/35476316:ICFP(283-311)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547631
Matsushita YDenis XJourdan JDreyer DJhala RDillig I(2022)RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe codeProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523704(841-856)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523704
Patterson DMushtak NWagner AAhmed AJhala RDillig I(2022)Semantic soundness for language interoperabilityProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523703(609-624)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523703
Spies SKrishnaswami NDreyer D(2021)Transfinite step-indexing for terminationProceedings of the ACM on Programming Languages10.1145/34342945:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434294
Jung RJourdan JKrebbers RDreyer D(2021)Safe systems programming in RustCommunications of the ACM10.1145/341829564:4(144-152)Online publication date: 22-Mar-2021
https://dl.acm.org/doi/10.1145/3418295
Beringer L(2021)Verified Software UnitsProgramming Languages and Systems10.1007/978-3-030-72019-3_5(118-147)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_5
Tahat AJoshi SGoswami PRavindran B(2019)Scalable Translation Validation of Unverified Legacy OS Code2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894252(1-9)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894252
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Semantic analysis of normalisation by evaluation for typed lambda calculus

A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F

Singleton: a general-purpose dependently-typed assembly language

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Funding Sources

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations