NDLI: A logic for reasoning with higher-order abstract syntax

Content Provider	IEEE Xplore Digital Library
Author	McDowell, R. Miller, D.
Copyright Year	1997
Description	Author affiliation: Dept. of Comput. & Inf. Sci., Pennsylvania Univ., Philadelphia, PA, USA (McDowell, R.)
Abstract	Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and inference systems. Given such specifications, it is natural to consider proving properties about the specified systems in the framework: for example, given the specification of evaluation for a functional programming language, prove that the language is deterministic or that the subject-reduction theorem holds. One challenge in developing a framework for such reasoning is that higher-order abstract syntax (HOAS), an elegant and declarative treatment of object-level abstraction and substitution, is difficult to treat in proofs involving induction. In this paper we present a meta-logic that can be used to reason about judgments coded using HOAS; this meta-logic is an extension of a simple intuitionistic logic that admits higher-order quantification over simply typed /spl lambda/-terms (key ingredients for HOAS) as well as induction and a notion of definition. The latter concept of a definition is a proof-theoretic device that allows certain theories to be treated as "closed" or as defining fixed points. The resulting meta-logic can specify various logical frameworks and a large range of judgments regarding programming languages and inference systems. We illustrate this point through examples, including the admissibility of cut for a simple logic and subject reduction, determinacy of evaluation, and the equivalence of SOS and natural semantics presentations of evaluation for a simple functional programming language.
Starting Page	434
Ending Page	445
File Size	1117444
Page Count	12
File Format	PDF
ISBN	0818679255
ISSN	10436871
DOI	10.1109/LICS.1997.614968
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1997-06-29
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Computer languages Functional programming Logic devices Logic programming Specification languages Information science Performance analysis
Content Type	Text
Resource Type	Article
Subject	Mathematics Software

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

Reasoning with Higher-Order Abstract Syntax in a Logical Framework

Combining Generic Judgments with Recursive Definitions

Approximate reasoning about the semantic effects of program changes

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

Reasoning with higher-order abstract syntax in a logical framework

A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs

A logic for reasoning with higher-order abstract syntax.

A congruence theorem for structured operational semantics of higher-order languages

Soft typing of general first-order languages

A logic for reasoning with higher-order abstract syntax

Similar Documents

Reasoning with Higher-Order Abstract Syntax in a Logical Framework

Combining Generic Judgments with Recursive Definitions

Approximate reasoning about the semantic effects of program changes

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

Reasoning with higher-order abstract syntax in a logical framework

A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs

A logic for reasoning with higher-order abstract syntax.

A congruence theorem for structured operational semantics of higher-order languages

Soft typing of general first-order languages

A logic for reasoning with higher-order abstract syntax