NDLI: A kripke logical relation between ML and assembly

Please wait, while we are loading the content...

Verified squared: does critical software deserve verified tools?

Points-to analysis with efficient strong updates

Relaxed-memory concurrency and verified compilation

Static analysis of multi-staged programs via unstaging translation

Step-indexed kripke models over recursive worlds

A shape analysis for optimizing parallel graph programs

The design of kodu: a tiny visual programming language for children on the Xbox 360

A separation logic for refining concurrent objects

The tree width of auxiliary storage

Automating string processing in spreadsheets using input-output examples

Multivariate amortized resource analysis

Making prophecies with decision predicates

Dynamic multirole session types

Robin Milner 1934--2010: verification, languages, and concurrency

Space overhead bounds for dynamic memory management with partial compaction

EigenCFA: accelerating flow analysis with GPUs

Loop transformations: convexity, pruning and optimization

Verifying higher-order functional programs with pattern-matching algebraic data types

A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code

Pick your contexts well: understanding object-sensitivity

Mathematizing C++ concurrency

Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol

A kripke logical relation between ML and assembly

Calling context abstraction with shapes

Correct blame for contracts: no more scapegoating

Modular reasoning for deterministic parallelism

Fresh-register automata

Predicate abstraction and refinement for verifying multi-threaded programs

Symmetric lenses

Delay-bounded scheduling

Practical affine types

Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated

Bisimulation for quantum processes

The essence of compiling with traces

Streaming transducers for algorithmic verification of single-pass list-processing programs

Learning minimal abstractions

Formal verification of object layout for c++ multiple inheritance

A parametric segmentation functor for fully automatic and scalable array content analysis

A typed store-passing translation for general references

Precise reasoning for programs using containers

Generative type abstraction and type-level computation

Expressive modular fine-grained concurrency specification

Vector addition system reachability problem: a short self-contained proof

Geometry of synthesis III: resource management through type inference

Regular expression containment: coinductive axiomatization and computational interpretation

On interference abstractions

Dynamic inference of static types for ruby

Complexity of pattern-based verification for multithreaded programs

Safe nondeterminism in a deterministic-by-default parallel language

Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code

Decidable logics combining heap structures and data

A kripke logical relation between ML and assembly

Content Provider	ACM Digital Library
Author	Hur, Chung-Kil Dreyer, Derek
Abstract	There has recently been great progress in proving the correctness of compilers for increasingly realistic languages with increasingly realistic runtime systems. Most work on this problem has focused on proving the correctness of a particular compiler, leaving open the question of how to verify the correctness of assembly code that is hand-optimized or linked together from the output of multiple compilers. This has led Benton and other researchers to propose more abstract, compositional notions of when a low-level program correctly realizes a high-level one. However, the state of the art in so-called "compositional compiler correctness" has only considered relatively simple high-level and low-level languages. In this paper, we propose a novel, extensional, compiler-independent notion of equivalence between high-level programs in an expressive, impure ML-like λ-calculus and low-level programs in an (only slightly) idealized assembly language. We define this equivalence by means of a biorthogonal, step-indexed, Kripke logical relation, which enables us to reason quite flexibly about assembly code that uses local state in a different manner than the high-level code it implements (e.g. self-modifying code). In contrast to prior work, we factor our relation in a symmetric, language-generic fashion, which helps to simplify and clarify the formal presentation, and we also show how to account for the presence of a garbage collector. Our approach relies on recent developments in Kripke logical relations for ML-like languages, in particular the idea of possible worlds as state transition systems.
Starting Page	133
Ending Page	146
Page Count	14
File Format	PDF MP4
ISBN	9781450304900
DOI	10.1145/1926385.1926402
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2011-01-26
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Garbage collection Self-modifying code Compositional compiler correctness Biorthogonality Step-indexed kripke logical relations
Content Type	Audio Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in