research-article

Biorthogonality, step-indexing and compiler correctness

Authors:

Chung-Kil HurAuthors Info & Claims

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

Pages 97 - 108

https://doi.org/10.1145/1596550.1596567

Published: 31 August 2009 Publication History

Abstract

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 stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.

Supplementary Material

JPG File (biorthogonalitystep-indexingandcompilercorrectnessonvimeo.jpg)

Download
20.56 KB

MP4 File (biorthogonalitystep-indexingandcompilercorrectnessonvimeo.mp4)

Download
93.41 MB

References

[1]

M. Abadi. TT-closed relations and admissibility. Mathematical Structures in Computer Science, 10(3), 2000.

Digital Library

[2]

M. Abadi. Protection in programming-language translations. In 25th International Colloquium on Automata, Languages and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science, 1998.

Digital Library

[3]

A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In 15th European Symposium on Programming (ESOP), volume 3924 of Lecture Notes in Computer Science, 2006.

Digital Library

[4]

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

Digital Library

[5]

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

Digital Library

[6]

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

[7]

A.W. Appel, P.-A. Mellies, C.D. Richards, and J. Vouillon. A Very Modal Model of a Modern, Major, General Type System. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2007.

Digital Library

[8]

N. Benton. Abstracting allocation: The new new thing. In 20th International Workshop on Computer Science Logic (CSL), volume 4207 of LNCS, 2006.

Digital Library

[9]

N. Benton and N. Tabareau. Compiling functional types to relational specifications for low level imperative code. In 4th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), 2009.

Digital Library

[10]

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

Digital Library

[11]

N. Benton, A. Kennedy, and C. Varming. Some domain theory and denotational semantics in Coq. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of Lecture Notes in Computer Science, 2009.

Digital Library

[12]

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

Digital Library

[13]

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

Digital Library

[14]

J. Guttman, J. Ramsdell, and M. Wand. VLISP: A verified implementation of scheme. Lisp and Symbolic Computation, 8(1/2), 1995.

Digital Library

[15]

T. Hardin, L. Maranget, and B. Pagano. Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming, 8, 1998.

Digital Library

[16]

A. Kennedy. Securing the .NET programming model. Theoretical Computer Science, 364(3), 2006.

Digital Library

[17]

J. L. Krivine. Classical logic, storage operators and second-order lambda calculus. Annals of Pure and Applied Logic, 1994.

[18]

P. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4), 1964.

[19]

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

Digital Library

[20]

X. Leroy and H. Grall. Coinductive big-step operational semantics. Information and Computation, 207(2), 2009.

Digital Library

[21]

J. Longley. When is a functional program not a functional program? In 4th ACM SIGPLAN International Conference on Functional Programming (ICFP), 1999.

Digital Library

[22]

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

[23]

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

[24]

G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5, 1977.

[25]

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

Digital Library

[26]

G.Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.

Digital Library

Cited By

Goncharov SMilius STsampas SUrbat HSobocinski PLago UEsparza J(2024)Bialgebraic Reasoning on Higher-order Program EquivalenceProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662099(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662099
Goncharov SSantamaria ASchröder LTsampas SUrbat H(2024)Logical Predicates in Higher-Order Mathematical Operational SemanticsFoundations of Software Science and Computation Structures10.1007/978-3-031-57231-9_3(47-69)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57231-9_3
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

Recommendations

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 ...
Proving Correctness of a Compiler Using Step-indexed Logical Relations

In this paper we prove the correctness of a compiler for a call-by-name language using step-indexed logical relations and biorthogonality. The source language is an extension of the simply typed lambda-calculus with recursion, and the target language is ...
A certified type-preserving compiler from lambda calculus to assembly language
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming

August 2009

364 pages

ISBN:9781605583327

DOI:10.1145/1596550

General Chair:
Graham Hutton
University of Nottingham
,
Program Chair:
Andrew Tolmach
Portland State University

ACM SIGPLAN Notices Volume 44, Issue 9
ICFP '09
September 2009
343 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1631687
Issue’s Table of Contents

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: 31 August 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '09

Sponsor:

ICFP '09: ACM SIGPLAN International Conference on Functional Programming

August 31 - September 2, 2009

Edinburgh, Scotland

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

98
Total Citations
View Citations
495
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)1

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Goncharov SMilius STsampas SUrbat HSobocinski PLago UEsparza J(2024)Bialgebraic Reasoning on Higher-order Program EquivalenceProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662099(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662099
Goncharov SSantamaria ASchröder LTsampas SUrbat H(2024)Logical Predicates in Higher-Order Mathematical Operational SemanticsFoundations of Software Science and Computation Structures10.1007/978-3-031-57231-9_3(47-69)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57231-9_3
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
Sammler MSpies SSong YD'Osualdo EKrebbers RGarg DDreyer D(2023)DimSum: A Decentralized Approach to Multi-language Semantics and VerificationProceedings of the ACM on Programming Languages10.1145/35712207:POPL(775-805)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571220
SULZMANN MWEHR S(2023)A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic GoJournal of Functional Programming10.1017/S095679682300004733Online publication date: 9-Oct-2023
https://doi.org/10.1017/S0956796823000047
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
Sulzmann MWehr S(2022)Semantic Preservation for a Type Directed Translation Scheme of Featherweight GoMathematics of Program Construction10.1007/978-3-031-16912-0_7(178-197)Online publication date: 22-Sep-2022
https://doi.org/10.1007/978-3-031-16912-0_7
Paraskevopoulou ZLi JAppel A(2021)Compositional optimizations for CertiCoqProceedings of the ACM on Programming Languages10.1145/34735915:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473591
Skorstengaard LDevriese DBirkedal L(2019)Reasoning about a Machine with Local CapabilitiesACM Transactions on Programming Languages and Systems10.1145/336351942:1(1-53)Online publication date: 10-Dec-2019
https://dl.acm.org/doi/10.1145/3363519
Patterson DAhmed A(2019)The next 700 compiler correctness theorems (functional pearl)Proceedings of the ACM on Programming Languages10.1145/33416893:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341689
Show More Cited By

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents