Guillaume FORTAINE
2007-01-14 19:25:06 UTC
Hello,
I believe that there are great thougths in this mail.However, I will try to
enhance it, because there are some major mistakes.
Michael FIG wrote Thu Aug 3 08:35:36 PDT 2006
Arrows are a new abstract view of computation, defined by John Hughes [Hug00].
They serve much the same purpose as monads -- providing a common structure
for libraries -- but are more general. In particular they allow notions of
computation that may be partially static (independent of the input) or may
take multiple inputs. If your application works fine with monads, you might
as well stick with them. But if you're using a structure that's very like a
monad, but isn't one, maybe it's an arrow.
http://www.dcs.st-and.ac.uk/~eb/esc.php
ESC, the Epigram Supercombinator Compiler, is a simple functional language
which compiles to efficient (well, maybe!) C code. The primary aim is to
develop a back end for Epigram, but it will (I hope, eventually) be useful to
anyone looking for a back end for a functional language.
http://repetae.net/john/computer/jhc/
jhc
jhc is a haskell compiler which aims to produce the most efficient programs
possible via whole program analysis and other optimizations
http://programatica.cs.pdx.edu/House/
Haskell User's Operating System and Environment, version 0.8, August 2006
House is a demo of software written in Haskell, running in a standalone
environment. It is a system than can serve as a platform for exploring
various ideas relating to low-level and system-level programming in a
high-level functional language. More details are available in our ICFP 2005
paper: A Principled Approach to Operating System Construction in Haskell.
http://en.wikipedia.org/wiki/FPGA
http://srg.cs.uiuc.edu/twiki/bin/view/OpenFPGA/
http://www.openfpga.org/
There are almost complete and FPGAs are available ;) !
I look forward to your answer,
Best Regards,
Guillaume
PS : I believe that we are near a fomally verified AI :
-Separation Logic :
http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html
http://www.bcs-facs.org/events/EveningSeminars/slides/richard_bornat_08_12_05-handouts.pdf
http://en.wikipedia.org/wiki/Separation_logic
Separation Logic a term attributed to John C. Reynolds, is an extension of
Hoare logic that describes variations on program logic in computer science.
In particular, separation logic facilitates reasoning about:
programs that manipulate pointer data structures — including information
hiding in the presence of pointers;
"transfer of ownership" (avoidance of semantic frame axioms); and
virtual separation (modular reasoning) between concurrent modules
-Deep Inference and the Calculus of Structures :
http://alessio.guglielmi.name/res/cos/LD/index.html
http://wwwhomes.doc.ic.ac.uk/~ozank/Papers/aia05.pdf
Towards Planning as Concurrency
Ozan Kahramanogullari
We present a purely logical framework to planning where we bring the
sequential and parallel composition in the plans to the same level, as in
process algebras. The problem of expressing causality, which is very
challenging for common logics and traditional deductive systems, is solved by
resorting to a recently developed extension of multiplicative exponential
linear logic with a self-dual, noncommutative operator. We present an
encoding of the conjunctive planning problems in this logic, and provide a
constructive soundness and completeness result. We argue that this work is
the first, but crucial, step of a uniform deductive formalism that connects
planning and concurrency inside a common language, and allow to transfer
methods from concurrency to planning.
I believe that there are great thougths in this mail.However, I will try to
enhance it, because there are some major mistakes.
Michael FIG wrote Thu Aug 3 08:35:36 PDT 2006
Hi,
I am a professional project manager and cybernetician. I have been
studying TUNES (http://www.tunes.org/) for several years, and have
come up with a project plan to accomplish it. I am running it past
you to see what you think, but honestly, I will work on it whether you
want to cooperate or not, as is my freedom with free software.
However, I would be happier if you joined me. :)
My home page (in my signature) fully explains my history and
intentions, which you can explore at your leisure.
6. Category Theory
5. Specification Language
4. Dynamic Compiler
3. Runtime Environment
2. Computational Model
1. Virtual Machine
0. Hardware
Here are the URLs of the best-of-breed free software I have chosen to
fulfill these requirements.
6. Arrow - http://tunes.org/~water/arrow/
Please see : http://www.haskell.org/arrows/I am a professional project manager and cybernetician. I have been
studying TUNES (http://www.tunes.org/) for several years, and have
come up with a project plan to accomplish it. I am running it past
you to see what you think, but honestly, I will work on it whether you
want to cooperate or not, as is my freedom with free software.
However, I would be happier if you joined me. :)
My home page (in my signature) fully explains my history and
intentions, which you can explore at your leisure.
6. Category Theory
5. Specification Language
4. Dynamic Compiler
3. Runtime Environment
2. Computational Model
1. Virtual Machine
0. Hardware
Here are the URLs of the best-of-breed free software I have chosen to
fulfill these requirements.
6. Arrow - http://tunes.org/~water/arrow/
Arrows are a new abstract view of computation, defined by John Hughes [Hug00].
They serve much the same purpose as monads -- providing a common structure
for libraries -- but are more general. In particular they allow notions of
computation that may be partially static (independent of the input) or may
take multiple inputs. If your application works fine with monads, you might
as well stick with them. But if you're using a structure that's very like a
monad, but isn't one, maybe it's an arrow.
5. Epigram - http://e-pig.org/
Please see :http://www.dcs.st-and.ac.uk/~eb/esc.php
ESC, the Epigram Supercombinator Compiler, is a simple functional language
which compiles to efficient (well, maybe!) C code. The primary aim is to
develop a back end for Epigram, but it will (I hope, eventually) be useful to
anyone looking for a back end for a functional language.
http://repetae.net/john/computer/jhc/
jhc
jhc is a haskell compiler which aims to produce the most efficient programs
possible via whole program analysis and other optimizations
4. Pliant - http://fullpliant.org/
3. Figure - http://fig.org/figure/figure.txt (also see The Circle of
the Promises http://fig.org/figure/CircleOfPromises.pdf.)
2. An amalgamation of the Mozart (http://www.mozart-oz.org/), E
(http://erights.org/), and Erlang (http://erlang.org/) models
1. Factor - http://factorcode.org/
You don't need 6 languages ! 1 will be enough :3. Figure - http://fig.org/figure/figure.txt (also see The Circle of
the Promises http://fig.org/figure/CircleOfPromises.pdf.)
2. An amalgamation of the Mozart (http://www.mozart-oz.org/), E
(http://erights.org/), and Erlang (http://erlang.org/) models
1. Factor - http://factorcode.org/
http://programatica.cs.pdx.edu/House/
Haskell User's Operating System and Environment, version 0.8, August 2006
House is a demo of software written in Haskell, running in a standalone
environment. It is a system than can serve as a platform for exploring
various ideas relating to low-level and system-level programming in a
high-level functional language. More details are available in our ICFP 2005
paper: A Principled Approach to Operating System Construction in Haskell.
0. Optical computers - http://en.wikipedia.org/wiki/Optical_computer
I believe that FPGAs will be better :http://en.wikipedia.org/wiki/FPGA
http://srg.cs.uiuc.edu/twiki/bin/view/OpenFPGA/
http://www.openfpga.org/
There are almost complete and FPGAs are available ;) !
I look forward to your answer,
Best Regards,
Guillaume
PS : I believe that we are near a fomally verified AI :
-Separation Logic :
http://www.dcs.qmul.ac.uk/~ohearn/localreasoning.html
http://www.bcs-facs.org/events/EveningSeminars/slides/richard_bornat_08_12_05-handouts.pdf
http://en.wikipedia.org/wiki/Separation_logic
Separation Logic a term attributed to John C. Reynolds, is an extension of
Hoare logic that describes variations on program logic in computer science.
In particular, separation logic facilitates reasoning about:
programs that manipulate pointer data structures — including information
hiding in the presence of pointers;
"transfer of ownership" (avoidance of semantic frame axioms); and
virtual separation (modular reasoning) between concurrent modules
-Deep Inference and the Calculus of Structures :
http://alessio.guglielmi.name/res/cos/LD/index.html
http://wwwhomes.doc.ic.ac.uk/~ozank/Papers/aia05.pdf
Towards Planning as Concurrency
Ozan Kahramanogullari
We present a purely logical framework to planning where we bring the
sequential and parallel composition in the plans to the same level, as in
process algebras. The problem of expressing causality, which is very
challenging for common logics and traditional deductive systems, is solved by
resorting to a recently developed extension of multiplicative exponential
linear logic with a self-dual, noncommutative operator. We present an
encoding of the conjunctive planning problems in this logic, and provide a
constructive soundness and completeness result. We argue that this work is
the first, but crucial, step of a uniform deductive formalism that connects
planning and concurrency inside a common language, and allow to transfer
methods from concurrency to planning.