NDLI: Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection

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

The development of Chez Scheme

Improving flow analyses via ΓCFA: abstract garbage collection and counting

Simple unification-based type inference for GADTs

From structures and functors to modules and units

Practical proofs of concurrent programs

Transactional events

Modular development of certified program verifiers with a proof assistant

Fifteen years of functional pearls

A pattern for almost compositional functions

Boxy types: inference for higher-rank types and impredicativity

Delimited dynamic binding

Polymorphism and separation in hoare type theory

The missing link: dynamic components for ML

Stabilizers: a modular checkpointing abstraction for concurrent functional programs

Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection

biXid: a bidirectional transformation language for XML

Algebraic fusion of functions with an accumulating parameter and its improvement

Access control in a core calculus of dependency

Static typing for a faulty lambda calculus

Recursive modules for programming

Static analysis for syntax objects

Modelling deterministic concurrent I/O

Equality of streams is a Π0 over 2-complete problem

Extensible programming with first-class cases

Programming monads operationally with Unimo

Abstraction preservation and subtyping in distributed languages

Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection

Content Provider	ACM Digital Library
Author	Hickey, Jason Nogin, Aleksey Yu, Xin Kopylov, Alexei
Abstract	We investigate the development of a general-purpose framework for mechanized reasoning about the meta-theory of programming languages. In order to provide a standard, uniform account of a programming language, we propose to define it as a logic in a logical framework, using the same mechanisms for definition, reasoning, and automation that are available to other logics. Then, in order to reason about the language's meta-theory, we use reflection to inject the programming language into (usually richer and more expressive) meta-theory.One of the key features of our approach is that structure of the language is preserved when it is reflected, including variables, meta-variables, and binding structure. This allows the structure of proofs to be preserved as well, and there is a one-to-one map from proof steps in the original programming logic to proof steps in the reflected logic. The act of reflecting a language is automated; all definitions, theorems, and proofs are preserved by the transformation and all the key lemmas (such as proof and structural induction) are automatically derived.The principal representation used by the reflected logic is higher-order abstract syntax (HOAS). However, reasoning about terms in HOAS can be awkward in some cases, especially for variables. For this reason, we define a computationally equivalent variable-free de Bruijn representation that is interchangeable with the HOAS in all contexts. The de Bruijn representation inherits the properties of substitution and alpha-equality from the logical framework, and it is not complicated by administrative issues like variable renumbering.We further develop the concepts and principles of proofs, provability, and structural and proof induction. This work is fully implemented in the MetaPRL theorem prover. We illustrate with an application to F<: as defined in the POPLmark challenge.
Starting Page	172
Ending Page	183
Page Count	12
File Format	PDF
ISBN	1595933093
DOI	10.1145/1159803.1159826
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2006-09-17
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Higher-order abstract syntax Type theory Languages with bindings Nuprl Mechanized reasoning Meta-theory Reflection Metaprl
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