Oliver,
Many thanks for the links to polycontextural logics. My feeling is it will take me quite some investment to get a feeling for the framework. In the meantime, there are fairly simple accounts of concurrency with reflection offering natural logics (without apparent liar's paradox issues, as i understand them).
At ETAPS 05 i presented two papers on such systems. You can find preprints here (http://svn.biosimilarity.com/src/open/papers/trunk/concurrency/rho/ex_nihilo_entcs/ex_nihilo_finco.pdf
; http://svn.biosimilarity.com/src/open/papers/trunk/concurrency/rho/tgc%20lncs/ex_nihilo_logic.pdf).
i did a quick and dirty OCaml implementation (as a way to learn OCaml), which you can find here (http://svn.biosimilarity.com/src/open/mirrororrim/rho/trunk/ocaml/
).
The approach i took was based on my dissatisfaction with the fact that the \pi-calculus was dependent on a theory of names; and, names had to have an effective theory of equality (thus, sneaking in a notion of computation -- which the \pi-calculus was supposedly providing the foundations of). If you formulate the situation as: given a set (resp. theory) of names, X, the \pi-calculus generates a set (resp. theory) of processes \Pi(X), then you can ask if the following domain equation has a solution
It does (lots of them). In the first paper cited i presented a minimal solution (least fixed point). The basic idea is to introduce a notion of quotation and dequotation. Quotation happens at communication (output appears higher-order, in that it has a process in subject position, but what is sent is the code or quote of the process). Likewise, dequotation is really only interesting at communction time, when it is bound by an input. (See the paper for the full story.)
In the second paper, i show that the (spatial logic version of the) standard Hennessy-Milner construction pushes through -- but with a pleasant surprise. In addition to formulae describing sets of processes, we find formulae describing sets of names. You get a whole logic of namespaces. One way to look at it is this: the algebraic operations on names inherited from the process algebraic combinators give you a pointer arithmetic. Fortunately, the programmer of such a system is also equipped with a logic that gives very potent means of reasoning about this pointer arithmetic. (Again, see the paper for the full story.)
The reflection doesn't just stop at structural reflection. You can provide a reflective comm rule in which even synchronization -- which is normally given via name-equality -- is determined by an upper-level reduction of the processes whose codes are the names being used to synchronize. Amazingly, this can be shown to be well-founded.
As a final point of interest, the first paper presents an encoding of the \pi-calculus into the reflective setting, demonstrating that both replication and the new-operator are syntactic sugar. There is a process algebraic form of the Y-combinator in the reflective setting that gives you replication. My co-author and i came up with two different encodings of the new-operator. His was 'centralized' but more elegant; mine was distributed, but with more machinery to make it work. But, i also found a 3rd encoding in which the well-founded recursion of quotation is replaced by non-well-founded forms. In this case, you obtain an interpretation of new that is strongly analogous to Galois extensions of a field.
Best wishes,
--greg
On 6/6/07, caml-list-request@yquem.inria.fr <
caml-list-request@yquem.inria.fr> wrote:Send Caml-list mailing list submissions to
caml-list@yquem.inria.fr
To subscribe or unsubscribe via the World Wide Web, visit
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
or, via email, send a message with subject or body 'help' to
caml-list-request@yquem.inria.fr
You can reach the person managing the list at
caml-list-owner@yquem.inria.fr
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Caml-list digest..."
Today's Topics:
1. Re: JoCaml Released. (Oliver Bandel)
2. Call for papers - IFL 2007 (Michel Mauny)
3. Re: re: We should all be forking (Oliver Bandel)
4. Re: JoCaml Released. (Oliver Bandel)
5. Re: JoCaml Released. (Jon Harrop)
---------- Forwarded message ----------
From: Oliver Bandel <oliver@first.in-berlin.de
>
To: caml-list@inria.fr
Date: Wed, 6 Jun 2007 11:00:38 +0200
Subject: Re: [Caml-list] JoCaml Released.
On Wed, Jun 06, 2007 at 10:18:15AM +0200, Oliver Bandel wrote:
> On Mon, Jun 04, 2007 at 10:13:55AM -0400, Joshua D. Guttman wrote:
> > Oliver Bandel <oliver@first.in-berlin.de> writes:
> >
> > >
> > >
> > > As far as I know only polycontextural logic can express
> > > parallel, distributed systems (and selfreference) in a
> > > complete/total way. So, when join calculus is
> > > monocontextural (which it is, if it uses the math we all
> > > have learned) it will be a subsystem of what can be
> > > expressed with polycontextural logic.
> > >
> >
> > Well, I googled and found the Wikipedia article on Gotthard
> > Guenther, which talked about trans-Aristotelian logic and
> > the law of the excluded middle (shades of Korzybski! Were
> > they connected?).
> >
> > But there was no indication what
> > monocontextural/polycontextural meant, or why only the
> > latter expresses distribution *completely*.
> >
> > Could you give a brief summary, please?
> [...]
>
> I answered to your private maila ddress twice.
> ...well oooh, I didn't saw you also wrote to this list.
>
>
> I will collect both mails and send it to the list today.
>
...is it interests other people...
Ciao,
Oliver
---------- Forwarded message ----------
From: Michel Mauny <Michel.Mauny@inria.fr
>
To: caml-list@inria.fr
Date: Wed, 06 Jun 2007 11:04:12 +0200
Subject: [Caml-list] Call for papers - IFL 2007
**********************************************************************
Announcement and Call for Papers for the
19th International Symposium on
Implementation and Application of Functional Languages
IFL 2007
27th-29th September 2007, Freiburg, Germany
co-located with ICFP 2007
http://proglang.informatik.uni-freiburg.de/IFL2007/
**********************************************************************
The aim of the IFL symposium is to bring together researchers actively
engaged in the implementation and application of functional and
function-based programming languages. The symposium provides an open
forum for researchers who wish to present and discuss new ideas and
concepts, work in progress, preliminary results, etc. related
primarily but not exclusively to the implementation and application of
functional languages.
Topics of interest include (but are not limited to):
* language concepts
* type checking
* compilation techniques
* (abstract) interpretation
* generic programming techniques
* automatic program generation
* array processing
* concurrent/parallel programming
* concurrent/parallel program execution
* heap management
* runtime profiling
* performance measurements
* debugging and tracing
* (abstract) machine architectures
* verification
* formal aspects
* tools and programming techniques
Papers on applications or tools demonstrating the suitability of novel
ideas in any of the above areas and contributions on related
theoretical work are also welcome. The change of the symposium name
adding the term "application", introduced in 2004, reflects the
broader scope IFL has gained over the years.
Contributions
Prospective authors are encouraged to submit papers to be published in
the draft proceedings and present them at the symposium. All
contributions must be written in English, conform to the
Springer-Verlag LNCS series format and not exceed 16 pages. The draft
proceedings will appear as a technical report.
Every attendee of IFL 2007 will have the opportunity to submit a
revised version of their paper for post-symposium reviewing. As in
previous years, selected papers will be published by Springer Verlag
in the Lecture Notes in Computer Science (LNCS) Series.
Important Dates
Submission for Draft Proceedings 31 August 2007
Early Registration Deadline 1 September 2007
Symposium 27-29 September 2007
Submission for post-refereeing 2 November 2007
Notification of acceptance / rejection 14 December 2007
Submission of camera-ready version 25 January 2008
Programme Committee
Peter Achten Radboud University Nijmegen, The Netherlands
Kenichi Asai Ochanomizu University, Japan
Manuel Chakravarty The University of New South Wales, Australia
Olaf Chitil (chair) University of Kent, UK
Martin Erwig Oregon State University, Oregon, USA
Marc Feeley Université de Montréal, Canada
Martin Gasbichler Zühlke Engineering AG, Switzerland
Kevin Hammond University of St. Andrews, Scotland
Zoltán Horváth Eötvös Loránd University, Budapest, Hungary
John Hughes Chalmers University of Technology, Sweden
Ken Friis Larsen University of Copenhagen, Denmark
Rita Loogen Philipps-Universität Marburg, Germany
Michel Mauny ENSTA, France
Sven-Bodo Scholz University of Hertfordshire, UK
Clara Segura Universidad Complutense de Madrid, Spain
Tim Sheard Portland State University, Oregon, USA
Glenn Strong Trinity College, Dublin, Ireland
Doaitse Swierstra Utrecht University, The Netherlands
Malcolm Wallace The University of York, UK
Local Organisation
Markus Degen Universität Freiburg, Germany
Peter Thiemann Universität Freiburg, Germany
Stefan Wehr Universität Freiburg, Germany
Further Information
http://proglang.informatik.uni-freiburg.de/IFL2007/
--
Michel Mauny
ENSTA
(+33) 1 4552 5388 (ENSTA)
(+33) 1 3963 5796 (INRIA)
---------- Forwarded message ----------
From: Oliver Bandel <oliver@first.in-berlin.de>
To:
caml-list@inria.fr
Date: Wed, 6 Jun 2007 11:28:40 +0200
Subject: Re: [Caml-list] re: We should all be forking
On Tue, Jun 05, 2007 at 03:30:47PM -0700, Christopher Cramer wrote:
> Jon Harrop:
> > I believe the performance relies upon the Linux kernel lazily copying
> > the process. Does OSX also do that?
>
> It's called copy-on-write and I would be surprised if OSX didn't also
> do it.
>
> The only way to start a new process is to fork, so even if you're just
> running another program you fork first, and then replace the process
> image with the new program with exec. If the fork had to copy the entire
> process image before just throwing it away upon exec, I think Unix,
> which is based around a philosophy of piping between multiple processes,
> would have abandoned fork a long time ago. Then again, there is vfork,
> so I guess they almost did abandon it at one point.
>
[...]
vfork is only (!!!) for a fork-exec combination.
So, be aware: do not use vfork, if you don't exec right after it!
Ciao,
Oliver
---------- Forwarded message ----------
From: Oliver Bandel <oliver@first.in-berlin.de>
To: caml-list@inria.fr
Date: Wed, 6 Jun 2007 11:31:25 +0200
Subject: Re: [Caml-list] JoCaml Released.
On Wed, Jun 06, 2007 at 11:22:42AM +0200, Francisco Jos? Valverde Albacete wrote:
> Come on! This is an open forum to learn... You just don't put in an idea
> only *not to explain it*.
Well, why is the default of this list, that Replies go to private mail account?!
And I got only one person sending an interested reply....
>
> Please explain what your suggestion was.
OK.
I will try my best.... it follows today.
Ciao,
Oliver
---------- Forwarded message ----------
From: Jon Harrop <jon@ffconsultancy.com>
To: caml-list@inria.fr
Date: Wed, 6 Jun 2007 10:40:57 +0100
Subject: Re: [Caml-list] JoCaml Released.
On Wednesday 06 June 2007 10:00:38 Oliver Bandel wrote:
> ...I will collect both mails and send it to the list today...
On Wednesday 06 June 2007 10:00:38 Oliver Bandel wrote:
> ...is it interests other people...
On Wednesday 06 June 2007 10:31:25 Oliver Bandel wrote:
> ...I will try my best.... it follows today...
The suspense is killing. ;-)
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?e
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives:
http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103
+1 206.650.3740
http://biosimilarity.blogspot.com