Re: [Haskell] Re: lambda calculus theory

[Greg Woodhouse]

A nice elementary treatment of typed lambda calculus can be found in "Types and Programming Languages" by Benjamin C. Pierce. My favorive introduction to compuytability theory is undoubtedly Barry S. Cooper's book, though it's pretty light on the lambda calculus. I understand that the first satisfactory model theoretic approach is due to Dana Scott, though I don't have access to it (yet). What I've been able to glean from more elementary treatments suggest that it focuses on replacing sets with more structured on objects known as domains, allowing recursive definitions to be formalized as fixpoints of continuous functions on lattices. I would love to find a reasonably accessible proof of the  Church-Rosser theorem. In lambda calculus, on "computes" by reducing lambda expressions according to one of three basic rules:
 
alpha reduction - allows renaming of free variables
beta - reduction - allows uniform substitution
eta reduction - allows irrelevevent abstractions to be dropped
 
But, though various evaluation strategies fix the order in which reductions are applied in real implementations, the lambda calculus does not specify any particular order, and the Church-Rosser theorem states that the "normal form" (_expression_ that cannot be reduced further) you reach, if any, is well-defined.
 
Another way to look at it is that pure functional languages do not fix an order in which "statements" are "executed", but consist of a series of definitions evaluated through reduction. That the result is well-defined in an imperative language is clear because there is usually a straightforward operational semantics. But the functional "machine" is more like a theorem prover, so you need something like a consistency theorem (as in logic) saying that the conclusion you might reach from a set of (conistent) premises is well-defined.
 
I hope this helps."Marc A. Ziegert" <[EMAIL PROTECTED]> wrote:
(this duplicates that inquiry from glasgow-haskell-users@ to haskell@)Am Sonntag, 6. November 2005 15:53 schrieb Hans N Beck:> Hi,> > I'm searching for a good mathematical oriented introduction to the > theory of lambda calculus or other theoretical foundations of Lisp/ > Haskell, i.e. monads or such (of course in the web there are much > hints, but what is the best for mathematicans foreign to this field)> > Regards> > Hans> ___> Glasgow-haskell-users mailing list> Glasgow-haskell-users@haskell.org> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users> > Hi Hans,i'm searching for such lectures/papers/scripts, too.well, untill there is a better answer, i send you some lin
 ks,
 which i think could be interesting to you.the first real mathematical definition of "monad", i read, was in the paper "The essence of dataflow programming". i approve to not omit that paper, if you like both, haskell and that theory.beside that, i attended a german lecture about Algebraic Topology. one chapter was about cathegory theory. it was not that much, but interesting.lambda:()very interesting is the "typed lambda calculus", which allows effective bug-prevention, which you do not have in most variants of lisp (or lisp's derivatives) but in haskell.functor:monad:there is a mathematical definition in the paper "The essence of dataflow programming", see 'comonad:' below.cathegory theory:arrow:comonad:beside these links, do not abstain from reading parts of the haskell library. (Data.Maybe, Data.Monoid, Control.Monad, Data.FunctorM, Control.Arrow)- marc___Haskell mailing listHaskell@haskell.orghttp://www.haskell.org/mailman/listinfo/haskell





===Gregory Woodhouse  <[EMAIL PROTECTED]>
"Einstein was a giant. He had his head in the clouds and his feet on the ground."
-- Richard P. Feynman
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Haskell-mode 2.1

[Stefan Monnier]

Haskell-mode 2.0 is now almost a year old, so I thought it was time to make
a new release.  You can find it at

http://www-perso.iro.umontreal.ca/~monnier/elisp/

This release has few visible changes.  Most of the changes are in the
haskell-indent module.  Those changes have not been heavily tested,
buyer beware: you get what you pay for.The intention is to make indentation
work better, but it's not always easy to guarantee forward progress.

Some of the changes have to do with making sure that the correct indentation
is among the provided indentation points (e.g. the `let' without `in'
in the `do' notation) while others try to trim the number of indentation
points (e.g. `in' has only one possible indentation point), and yet others
allow finer control (e.g. the haskell-indent-after-keywords variable which
allows to indent each branch of a `case' (or `where') by some 2 spaces).
Please report any unexpected behavior.

See appended the NEWS file that describes some of the noteworthy changes.


Stefan


Changes since 2.0:

* inf-haskell uses ghci if hugs is absent.

* Fix up some binding conflicts (C-c C-o in haskell-doc)

* Many (hopefully minor) changes to the indentation.

* New symbols in haskell-font-lock-symbols-alist.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: lambda calculus theory

[Ben Horsfall]

On 08/11/05, Marc A. Ziegert <[EMAIL PROTECTED]> wrote:
> (this duplicates that inquiry from glasgow-haskell-users@ to haskell@)
>
> Am Sonntag, 6. November 2005 15:53 schrieb Hans N Beck:
> > I'm searching for a good mathematical oriented introduction to the
> > theory of lambda calculus or other theoretical foundations of Lisp/
> > Haskell, i.e. monads or such (of course in the web there are much
> > hints, but what is the best for mathematicans foreign to this field)

On lambda calculus, have a look at:

H. P. Barendregt, Lambda Calculi with Types, in S. Abramsky and Dov M.
Gabbay and T. S. E. Maibaum, eds., Handbook of Logic in Computer
Science, Volume 2, Clarendon Press, Oxford, 1992, pp. 117--309

J. Roger Hindley and Jonathan P. Seldin, Introduction to Combinators
and $\lambda$-Calculus, Cambridge University Press, Cambridge, 1986.

A nice, standard introduction to category theory is:

Saunders Mac Lane, Categories for the Working Mathematician,
Springer-Verlag, New York, second edition, 1998.


Ben
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Re: lambda calculus theory

[Malcolm Wallace]

"Marc A. Ziegert" <[EMAIL PROTECTED]> writes:

> > I'm searching for a good mathematical oriented introduction to the  
> > theory of lambda calculus or other theoretical foundations of Lisp/ 
> > Haskell, i.e. monads or such (of course in the web there are much  
> > hints, but what is the best for mathematicans foreign to this field)
> 
> i'm searching for such lectures/papers/scripts, too.

The classic textbook on lambda calculus is 

The Lambda Calculus: Its Syntax and Semantics.
Henk Barendregt.
(Hardback, Elsevier, 1981)
(Paperback, North Holland, Amsterdam, 1987)

http://www.cs.ru.nl/~henk/
http://www.andrew.cmu.edu/user/cebrown/notes/barendregt.html

Regards,
Malcolm
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: lambda calculus theory

[Marc A. Ziegert]

(this duplicates that inquiry from glasgow-haskell-users@ to haskell@)



Am Sonntag, 6. November 2005 15:53 schrieb Hans N Beck:
> Hi,
> 
> I'm searching for a good mathematical oriented introduction to the  
> theory of lambda calculus or other theoretical foundations of Lisp/ 
> Haskell, i.e. monads or such (of course in the web there are much  
> hints, but what is the best for mathematicans foreign to this field)
> 
> Regards
> 
> Hans
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> 
> 



Hi Hans,

i'm searching for such lectures/papers/scripts, too.
well, untill there is a better answer, i send you some links, which i think 
could be interesting to you.
the first real mathematical definition of "monad", i read, was in the paper 
"The essence of dataflow programming". i approve to not omit that paper, if you 
like both, haskell and that theory.
beside that, i attended a german lecture about Algebraic Topology. one chapter 
was about cathegory theory. it was not that much, but interesting.


lambda:

()
very interesting is the "typed lambda calculus", which allows effective 
bug-prevention, which you do not have in most variants of lisp (or lisp's 
derivatives) but in haskell.

functor:


monad:
there is a mathematical definition in the paper "The essence of dataflow 
programming", see 'comonad:' below.

cathegory theory:





arrow:



comonad:



beside these links, do not abstain from reading parts of the haskell library. 
(Data.Maybe, Data.Monoid, Control.Monad, Data.FunctorM, Control.Arrow)



- marc

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] TYPES 06: Call for papers

[Wouter Swierstra]

  TYPES 2006

Main Conference of the Types Project
   Nottingham, UK, 18-24 April 2006

  http://www.cs.nott.ac.uk/types06/


This is the latest meeting in a series that started 1992, the last
conference was in December 2004 in Paris.

The topic of the meeting is formal reasoning and computer programming
based on Type Theory : languages and computerised tools for reasoning,
and applications in several domains such as analysis of programming
languages, certified software, formalisation of mathematics and
mathematics education.

TYPES 2006 is colocated with TFP 2006 (Trends in Functional
Programming) and we plan to hold a joint session on Dependently Typed
Programming.

The conference takes place at Jubilee campus of the University of
Nottingham, on-site accomodation will be available together with the
registration.

For more information see:  http://www.cs.nott.ac.uk/types06/

We will open registration early next year. You will be able to submit
your talk and abstract together with your registration. We will try to
accomodate all talks which fit into the scope of the TYPES
project. There will also be invited lectures.

Please direct all emails related to TYPES 2006 to
[EMAIL PROTECTED]

Cheers,

The Organisation Comittee

Thorsten Altenkirch, James Chapman, Conor McBride, Peter Morris and  
Wouter Swiestra




This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] POPL 2006 Call for Participation

[David Walker]

*
*  ACM SIGPLAN-SIGACT Symposium *
* on*
*   Principles of Programming Languages *
*   *
* January 11-13, 2006   *
*Charleston Place Hotel *
*  Charleston, South Carolina   *
*   *
*Call for Participation *
*   *
*http://www.cs.princeton.edu/~dpw/popl/06/  *
*

Important dates

* Early Registration Deadline: December 10, 2005 
* Hotel Reservation Deadline:  December 10, 2005 
* Conference:  January 11-13, 2006


Scope

The annual Symposium on Principles of Programming Languages is a forum for
the discussion of fundamental principles and important innovations in the
design, definition, analysis, transformation, implementation and
verification of programming languages, programming systems, and programming
abstractions. Both experimental and theoretical papers on principles and
innovations are welcome, ranging from formal frameworks to reports on
practical experiences.


Invited Speakers

* James McKinna, St Andrews University
* Martin Odersky, Ecole Polytechnique Fédérale de Lausanne
* Tim Sweeney, Epic Games Inc


Conference Registration

Registration is now open!  To register, please go to our registration site
at (http://www.regmaster.com/popl2006.html)  Early registration for a
reduced fee is available until December 10, 2005.  Don't delay!


Hotel Room Reservation

We recommend staying at the Charleston Place Hotel, which is where the
conference will be held.  Our group rate for the hotel is $155/night.  (This
does not include the 12.5% state tax on hotels.)  Please mention the group
name "ACM POPL 2006 Conference" when reserving a room.  You may reserve
rooms by phone, fax or email, but not using the web.

* phone: (800) 831-3490 -- Staffed Monday through Friday, 8:00 am to 6:00 pm

* fax: (843) 724-7215 
* email: [EMAIL PROTECTED]

The hotel website is
http://www.charlestonplace.com/web/ocha/ocha_a1a_splash.jsp


Student Attendees

Students who have a paper accepted for the conference are offered student
membership of SIGPLAN free for one year. As members of SIGPLAN they may
apply for travel fellowships from the PAC fund.


Conference Chair

Greg Morrisett
Harvard University
33 Oxford Street
Cambridge, MA 02138 USA
greg at eecs dot harvard dot edu

Program Chair

Simon Peyton Jones
Microsoft Research Ltd,
7 JJ Thomson Ave,
Cambridge CB3 0FB, UK
[EMAIL PROTECTED] 

Program Committee

* Giuseppe Castagna, CNRS, LIENS, ENS Paris
* Manuel Chakravarty, University of New South Wales
* Karl Crary, Carnegie Mellon University
* Sophia Drossopoulou, Imperial College London
* Paul Feautrier, ENS Lyon
* Carl A Gunter, University of Illinois
* Rajiv Gupta, University of Arizona
* Fritz Henglein, DIKU, University of Copenhagen
* Trevor Jim, AT&T
* Shriram Krishnamurthi, Brown University
* Gary T Leavens, Iowa State
* Robert O'Callahan, Novell
* Peter O'Hearn, Queen Mary, University of London
* Andreas Podelski, Max Planck Institute, Saarbrücken
* Andrei Sabelfeld, Chalmers University
* Kostis Sagonas, Uppsala University
* Davide Sangiorgi, University of Bologna
* Philip Wadler, University of Edinburgh
* Stephanie Weirich, University of Pennsylvania
* Hongwei Xi, Boston University


Affiliated Events

* Foundations of Object Oriented Languages (FOOL)
* January 14, 2006

* Partial Evaluation and Semantics-Based Program Manipulation (PEPM)
* January 9-10, 2006

* Practical Applications of Declarative Languages (PADL)
* January 9-10, 2006 

* Programming Language Technologies for XML (PLAN-X)
* January 14, 2006

* Semantics, Program Analysis and Computing Environments
  for Memory Management (SPACE 2006)
* January 14, 2006

* Verification, Model Checking and Abstract Interpretation (VMCAI)
* January 8-10, 2006


POPL 2006 Preliminary Program

Wednesday January 11, 2006
 08:30
 Invited talk
 Martin Odersky
 Ecole Polytechnique Fédérale de
Lausanne 
 
 10:00
 Staged Allocation: A Compositional Technique for Specifying and
Implementing Procedure Calling Conventions
 Reuben Olinsky, Christian Lindig and Norman Ramsey
 Harvard University
 
 10:25
 A Hierarchical Model of Data Locality
 Chengliang Zhang, Yutao Zhong, Mitsunori Ogihara, Chen Ding
 University of Rochester
 
 10:50
 Simplifying Reductions
 Gautam Gupta and Sanjay Rajopadhye
 Colorado State University

 11:40
 Formal certification of a compiler back-end, or: programming a compiler
with