Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Higher-order abstract syntax in classical higher-order logic
Howe D.  LFMTP 2009 (Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Montreal, Quebec, Canada, Aug 2, 2009)1-11.2009.Type:Proceedings
Date Reviewed: Apr 19 2010

It is remarkable how apparently simple ideas can be difficult to formalize. A bound variable--a variable that has a scope, such as the body of the function for which it is a parameter--is a case in point. When the lambda calculus was emerging in the 1930s and 1940s, more than one of the pioneers tripped up defining precisely how one expression could be substituted for a variable, without the structure of the bound variables changing, and “capture” perhaps taking place. This was, of course, resolved in time, but it’s interesting to observe that even now, mathematicians will use informal strategies, such as the Barendregt convention, to deal with bound variables in practice.

So, it should be perhaps less of a surprise to learn that dealing with variable binding inside computer systems using formal languages--such as the interactive theorem provers Isabelle, HOL, and Coq--is by no means straightforward. There are two general approaches. The first represents variables as objects of the metalanguage (the language in which the logic is formalized). This can be done by using strings, numbers (or de Bruijn indices), or other more complex approaches; each requires users to think explicitly about variable names--there’s no Barendregt convention inside a theorem prover! The other approach is to identify the variables to be modeled with variables in the metalanguage; it is to this tradition that this paper belongs.

Without going into detail, this approach works by identifying functions with bound variables as a new kind of function in the metalanguage. These are functions that--following the definition of Reynolds--are parametric, which in this case means that they purely construct values, without analyzing their inputs. This construction can then support the construction of least-fixed points to model recursive type definitions, a sticking point of previous approaches.

While deeply technical, the paper is very clearly written and the introduction provides a very clear summary of the various syntactic approaches, as well as the motivation for the work that it introduces.

Reviewer:  Simon Thompson Review #: CR137915 (1103-0299)
Bookmark and Share
  Featured Reviewer  
 
Semantics (D.3.1 ... )
 
 
Inference Engines (I.2.3 ... )
 
 
Proof Theory (F.4.1 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Mathematical Logic (F.4.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Semantics": Date
The semantics of programming languages: an elementary introduction using structural operational semantics
Hennessy M., John Wiley & Sons, Inc., New York, NY, 1990. Type: Book (9780471927723)
Jul 1 1991
Logic of domains
Zhang G., Birkhäuser Boston Inc., Cambridge, MA, 1991. Type: Book (9780817635701)
Mar 1 1993
A linear-history semantics for languages for distributed programming
Francez N., Lehmann D., Pnueli A. Theoretical Computer Science 32(1-2): 25-46, 1984. Type: Article
Jul 1 1985
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy