NDLI: A fold/unfold transformation framework for rewrite theories extended to CCT

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

Corrective hints for type incorrect generic Java programs

PET: a partial evaluation-based test case generation tool for Java bytecode

Optimizing generics is easy!

Regular approximation and bounded domains for size-change termination

Optimizing relational algebra operations using generic equivalence discriminators and lazy products

I/O guided detection of list catamorphisms: towards problem specific use of program templates in IP

Clone detection and elimination for Haskell

Context-sensitive analysis of obfuscated x86 executables

The SourceGraph program

O, partial evaluator, where art thou?

Mnemonics: type-safe bytecode generation at run time

IGOR2 - an analytical inductive functional programming system: tool demo

A fold/unfold transformation framework for rewrite theories extended to CCT

A3PAT, an approach for certified automated termination proofs

Programming with singular and plural non-deterministic functions

Bridging the gap between symbolic and efficient AES implementations

Making "stricterness" more relevant

Conditional weighted pushdown systems and applications

From higher-order logic to Haskell: there and back again

General purpose languages should be metalanguages

A fold/unfold transformation framework for rewrite theories extended to CCT

Content Provider	ACM Digital Library
Author	Alpuente, María Baggi, Michele Falaschi, Moreno Ballis, Demis
Abstract	Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with functions, rules, equations, sorts, and algebraic laws (such as commutativity and associativity). We provide correctness results for the transformation system w.r.t. the semantics of ground reducts. Moreover, we show how our transformation technique can be naturally applied to implement a Code Carrying Theory (CCT) system. CCT is an approach for securing delivery of code from a producer to a consumer where only a certificate (usually in the form of assertions and proofs) is transmitted from the producer to the consumer who can check its validity and then extract executable code from it. Within our framework, the certificate consists of a sequence of transformation steps which can be applied to a given consumer specification in order to automatically synthesize safe code in agreement with the original requirements. We also provide an implementation of the program transformation framework in the high-performance, rewriting logic language Maude which, by means of an experimental evaluation of the system, highlights the potentiality of our approach.
Starting Page	43
Ending Page	52
Page Count	10
File Format	PDF
ISBN	9781605587271
DOI	10.1145/1706356.1706367
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-01-19
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Code carrying theory Fold/unfold transformation Rewriting logic
Content Type	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