Re: [Haskell] A road for Haskell into the kernel of a full-fledged OS

2006-06-02 Thread Greg Buchholz
Joel Reymont wrote:
> 
> I think this is an awesome idea. I believe the folks at Galois have  
> customized the Haskell runtime for embedded devices but... I wonder  
> if us mere mortals will spend more time fighting laziness (and thus  
> high memory usage) than focusing on driver functionality.

In a similar vein, the Coyotos Project ( http://coyotos.org/ ) is 
writing their own language, BitC, to support their microkernel...

http://www.coyotos.org/docs/bitc/spec.html

"BitC is conceptually derived in various measure from Standard ML,
Scheme, and C. Like Standard ML [10], BitC has a formal semantics,
static typing, a type inference mechanism, and type variables. Like
Scheme [8], BitC uses a surface syntax that is readily represented as
BitC data. Like C [1], BitC provides full control over data structure
representation, which is necessary for high-performance systems
programming. The BitC language is a direct expression of the typed
lambda calculus with side effects, extended to be able to reflect the
semantics of explicit representation."


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


Re: [Haskell] A road for Haskell into the kernel of a full-fledged OS

2006-06-02 Thread Joel Reymont


On Jun 2, 2006, at 5:41 PM, [EMAIL PROTECTED] wrote:


It is quite instructive to compare a device driver in Haskell
with the original C driver -- it terms of length, speed, time to
write, number of bugs, etc.


I think this is an awesome idea. I believe the folks at Galois have  
customized the Haskell runtime for embedded devices but... I wonder  
if us mere mortals will spend more time fighting laziness (and thus  
high memory usage) than focusing on driver functionality.


Thanks, Joel

--
http://wagerlabs.com/





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


[Haskell] CFP: 2nd Int'l Workshop on Automated Specification and Verification of Web Systems (WWV'06)

2006-06-02 Thread Santiago Escobar

  [ We apologize for multiple copies ]

***

2nd International Workshop on Automated
 Specification and Verification
  of Web Systems (WWV'06)

   Cyprus, November 15-19, 2006
  (Track of ISoLA 2006)

 http://www.dsic.upv.es/workshops/wwv06

***

SCOPE

The  increased  complexity  of Web sites and the explosive growth of
Web-based applications has turned their design and construction into
a  challenging problem. Nowadays, many companies have diverted their
Web   sites   into   interactive,   completely-automated,  Web-based
applications (such  as  Amazon, on-line banking, or travel agencies)
with  a  high complexity that requires appropriate specification and
verification  techniques and tools. Systematic, formal approaches to
the  analysis  and  verification  can  address  the problems of this
particular  domain  with  automated  and  reliable  tools  that also
incorporate semantic aspects.

We solicit paper on formal methods and techniques applied to Web
sites, Web services or Web-based applications, such as:

 * rule-based approaches to Web site analysis, certification,
   specification, verification, and optimization
 * formal models for describing and reasoning about Web sites
 * model-checking, synthesis and debugging of Web sites
 * abstract interpretation and program transformation applied
   to the semantic Web
 * intelligent tutoring and advisory systems for Web specifications
   authoring

The WWV series provides a forum for researchers from the communities
of Rule-based programming, Automated Software Engineering, and
Web-oriented research to facilitate the cross-fertilization and the
advancement of hybrid methods that combine the three areas.

LOCATION

WWV'06 will be held in November in Cyprus as a Special Track
of the 2006 International Symposium on Leveraging Applications of
Formal Methods, Verification, and Validation (ISoLA 2006).

HISTORY

The first WWV'05 edition was held in Valencia, Spain, during March
14-15, 2005. The workshop was attended by 42 participants
from universities, research institutes, and companies from 11 countries:
Austria, Canada, France, Germany, India, Italy, Japan, Mexico, Spain,
UK, and USA. A selection of the papers appeared as a volume of the
Elsevier series Electronic Notes in Theoretical Computer Science (ENTCS).

SUBMISSION PROCEDURE

Submissions must be received by July 16, 2006. In addition, an ASCII
version of the title and abstract must have been submitted by July 3, 2006.
Submitted papers should be at most 15 pages in the Lecture Notes in
Computer Science (LNCS) style. Submitted papers should include an abstract
and the author's information. See the author's instructions of LNCS style
at http://www.springer.de/comp/lncs/authors.html.

PUBLICATION

Accepted papers will be published in a preliminary proceedings volume,
which will be available during the workshop. Publication of the
workshop post-proceedings in the Springer series Lecture Notes in
Computer Science (LNCS) is envisaged.

PROGRAM CO-CHAIRS

Maria Alpuente (Technical University of Valencia, Spain)
Moreno Falaschi (University of Siena, Italy)

WORKSHOP CHAIR

Santiago Escobar (Technical University of Valencia, Spain)

PROGRAM COMMITTEE

Jose Julio Alferes (Universidade Nova de Lisboa, Portugal)
Maria Alpuente (Technical University of Valencia, Spain)
Demis Ballis (University of Udine, Italy)
Francois Bry (University of Munich, Germany)
Santiago Escobar (Technical University of Valencia, Spain)
Francois Fages (INRIA Rocquencourt, France)
Moreno Falaschi (University of Siena, Italy)
Gopal Gupta (University of Texas at Dallas, USA)
Shriram Krishnamurthi (Brown University, USA)
Tiziana Margaria (University of Potsdam, Germany)
I.V. Ramakrishnan (State University of New York at Stony Brook, USA)
Leon van der Torre (University of Luxembourg, Luxembourg)

IMPORTANT DATES

Abstract Submission July 3, 2006
Full Paper Submission   July 16, 2006
Acceptance Notification September 17, 2006
Camera ReadyOctober 15, 2006
WorkshopNovember 15-19, 2006 (one day)

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


[Haskell] A road for Haskell into the kernel of a full-fledged OS

2006-06-02 Thread oleg

I'm attending a USENIX conference and just had a nice talk
with Andrew Tanenbaum. As some may know, he's working on the new
version of Minix, Minix3. It is actually working, now with the X
windows interface:

http://www.minix3.org

Andrew Tanenbaum said that it is important for a language like OCaml
or Haskell to get more visibility among the OS developers; and Minix
offers a very good way to do that. Minix3 is based on micro-kernel;
all of the OS services (memory manager, file system, all the drivers,
etc.) run as regular processes communicating through a well-defined
protocol. It is irreleveant what language these services are written
in, so long as they obey the protocol. Some of Andrew Tanenbaum's
students are interested in re-writing some of Minix3 OS services (like
device drivers or file systems, currently written in C) in Ocaml and
Cyclone. He is interested in the outcome. Haskell is a good candidate
too. It is quite instructive to compare a device driver in Haskell
with the original C driver -- it terms of length, speed, time to
write, number of bugs, etc. Andrew Tananbaum suggested that the
terminal driver may be the best start, because it is 
quite stand-alone, small and its protocol is simple.

With Minix, we can replace one kernel service of the
full-fledged, working OS with the one written in Haskell -- and
immediately see how it all works. If it doesn't, the rest of OS still
works and so we can unload the faulty service and load another
implementation. Minix3 does indeed offer an easy road to the OS kernel 
for a language other than C. I said that there may be quite a bit of
interest in Haskell community in such a project. I wonder if I'm
right...

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