research-article

Compiling functional types to relational specifications for low level imperative code

Authors:

Nicolas TabareauAuthors Info & Claims

TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementation

Pages 3 - 14

https://doi.org/10.1145/1481861.1481864

Published: 24 January 2009 Publication History

Abstract

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and separation, over stores and values in the low-level machine.

References

[1]

A. Ahmed. Semantics of types for mutable state. PhD thesis, Princeton University, Princeton, NJ, USA, 2004.

Digital Library

[2]

A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. In Proc. 13th ACM International Conference on Functional Programming (ICFP '08). ACM, 2008.

Digital Library

[3]

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In Proc. 36th ACM Symposium on Principles of Programming Languages (POPL '09), 2009.

Digital Library

[4]

A. Appel. Foundational proof-carrying code. In Proc. 16th IEEE Symposium on Logic in Computer Science (LICS), 2001.

Digital Library

[5]

A. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(5), 2001.

Digital Library

[6]

A.W. Appel, P.-A. Melliès, C.D. Richards, and J. Vouillon. A very modal model of a modern, major, general type system. Proc. 34th ACM Symposium on Principles of Programming Languages (POPL '07), pages 109--122, 2007.

Digital Library

[7]

N. Benton. Abstracting allocation: The new new thing. In CSL '06, volume 4207 of LNCS. Springer-Verlag, September 2006.

Digital Library

[8]

N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In Proc. 7th International Conference on Typed Lambda Calculi and Applications (TLCA), volume 3461 of Lecture Notes in Computer Science, 2005.

Digital Library

[9]

N. Benton and U. Zarfaty. Formalizing and verifying semantic type soundness of a simple compiler. In Proc. 9th ACM International Conference on Principles and Practice of Declarative Programming (PPDP '07), pages 1--12, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-769-8.

Digital Library

[10]

A. Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In Proc. 2007 ACM Conference on Programming Language Design and Implementation (PLDI '07), 2007.

Digital Library

[11]

M. Dave. Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes, 28(6), 2003.

Digital Library

[12]

R. Davies and F. Pfenning. Intersection types and computational effects. In Proc. 5th ACM International Conference on Functional Programming (ICFP '00), 2000.

Digital Library

[13]

N. Glew. Object closure conversion. In 3rd International Workshop on Higher Order Operational Techniques in Semantics, 1999.

[14]

X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL '06), 2006.

Digital Library

[15]

J. McCarthy and J. Painter. Correctness of a Compiler for Arithmetic Expressions. Proceedings Symposium in Applied Mathematics, 19:33--41, 1967.

[16]

Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proc. 23rd ACM Symposium on Principles of Programming Languages (POPL '96), pages 271--283, New York, NY, USA, 1996. ACM. ISBN 0-89791-769-3.

Digital Library

[17]

J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Trans. Program. Lang. Syst., 10(3), 1988.

Digital Library

[18]

Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL), 2006.

Digital Library

[19]

A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics. CUP, 1998.

Digital Library

[20]

J.C. Reynolds. Separation logic: A logic for shared mutable data structures. 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), pages 55--74, 2002.

Digital Library

[21]

N. Tabareau. Modalités de Ressource et Contrôle en Logique Tensorielle. PhD thesis, Université Paris Diderot (Paris 7), 2008.

[22]

G. Tan, A. Appel, K. Swadi, and D. Wu. Construction of a semantic model for a typed assembly language. In Proc. 5th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '04), 2004.

[23]

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

Digital Library

[24]

H. Yang. Relational separation logic. Theoretical Computer Science, 375 (1-3), 2007.

Digital Library

[25]

D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 50, 2004.

Digital Library

Cited By

Wagner AEisbach ZAhmed A(2024)Realistic Realizability: Specifying ABIs You Can Count OnProceedings of the ACM on Programming Languages10.1145/36897558:OOPSLA2(1249-1278)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689755
Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
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
Show More Cited By

Index Terms

Compiling functional types to relational specifications for low level imperative code
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Functional constructs
      2. Type structures
    2. Program reasoning
      1. Program specifications
      2. Program verification

Recommendations

Formalizing and verifying semantic type soundness of a simple compiler
PPDP '07: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized assembly language. Types in the high-level language are interpreted as ...
High-level separation logic for low-level code
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Separation logic is a powerful tool for reasoning about structured, imperative programs that manipulate pointers. However, its application to unstructured, lower-level languages such as assembly language or machine code remains challenging. In this ...
Biorthogonality, step-indexing and compiler correctness
ICFP '09

We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

TLDI '09: Proceedings of the 4th international workshop on Types in language design and implementation

January 2009

122 pages

ISBN:9781605584201

DOI:10.1145/1481861

General Chair:
Andrew Kennedy
Microsoft Research Cambridge, UK
,
Program Chair:
Amal Ahmed
Toyota Technological Institute at Chicago, USA

Copyright © 2009 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 January 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL09

Sponsor:

POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 24, 2009

GA, Savannah, USA

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
159
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wagner AEisbach ZAhmed A(2024)Realistic Realizability: Specifying ABIs You Can Count OnProceedings of the ACM on Programming Languages10.1145/36897558:OOPSLA2(1249-1278)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689755
Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
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
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
de Groot JLitak TPattinson DGorla D(2021)Gödel-McKinsey-Tarski and Blok-Esakia for Heyting-Lewis implicationProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470508(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470508
Benton NSabel DThiemann P(2018)Semantic Equivalence Checking for HHVM BytecodeProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236975(1-8)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236975
Kimmitt JGreaves DCirstea M(2015)A toolchain for safety-critical embedded processor programming using FPGAs2015 IEEE 13th International Conference on Industrial Informatics (INDIN)10.1109/INDIN.2015.7281847(848-855)Online publication date: Jul-2015
https://doi.org/10.1109/INDIN.2015.7281847
Wang PCuellar SChlipala A(2014)Compiler verification meets cross-language linking via data abstractionACM SIGPLAN Notices10.1145/2714064.266020149:10(675-690)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2714064.2660201
Wang PCuellar SChlipala ABlack AMillstein T(2014)Compiler verification meets cross-language linking via data abstractionProceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications10.1145/2660193.2660201(675-690)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2660193.2660201
Litak T(2014)Constructive Modalities with Provability SmackLeo Esakia on Duality in Modal and Intuitionistic Logics10.1007/978-94-017-8860-1_8(187-216)Online publication date: 4-Jun-2014
https://doi.org/10.1007/978-94-017-8860-1_8
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten