NDLI: Higher-order semantic labelling for inductive datatype systems

Content Provider	ACM Digital Library
Author	Hamana, Makoto
Abstract	We give a novel transformation for proving termination of higher-order rewrite systems in the format of Inductive Data Type Systems (IDTSs) by Blanqui, Jouannaud and Okada. The transformation called higher-order semantic labelling attaches algebraic semantics of the arguments to each function symbol. We systematically define the labelling and show that labelled systems give termination models in the frame-work of Fiore, Plotkin and Turi's binding algebras. As applications, we give simple proofs of termination of the explicit substitution system λ X and currying transformation via higher-order semantic labelling. Moreover, we prove a new result of modularity of termination of IDTSs by introducing the notion of solid IDTSs. We prove that termination is preserved under the disjoint union of an IDTS and a higher-order program scheme.
Starting Page	97
Ending Page	108
Page Count	12
File Format	PDF
ISBN	9781595937698
DOI	10.1145/1273920.1273933
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2007-07-14
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Higher-order abstract syntax Categorical semantics Initial algebra semantics Termination Higher-order rewriting Modularity
Content Type	Text
Resource Type	Article

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

Higher-order semantic labelling for inductive datatype systems