non-deterministic lambda-calculus ?

[Francois-Rene Rideau]

Abstract:
   I am looking for papers describing some variant of the lambda-calculus.

Dear Functional programmers,

   last year, during my DEA, I developed an abstract model to do
reflective computations/proofs, using untyped rather than typed
lambda calculus (with integration into proof system for Scheme
programs in mind).

The computational core of the model was what I call
"non-deterministic, call-by-value lambda-calculus" (ND-\lambda_v),
whereby the semantics of a form, called its (logical) type
is (intuitively) the set of ("actual") values to which it may evaluate.
A form is "fully evaluated" to a single value (if exists, else it diverges)
before it may be passed as an argument to a function,
which I believe is to be called "committed-choice non-determinism"
as in Mercury (thousand thanks go to Fergus Henderson).

Non-deterministism appears as either new constructors or new functions,
either way being macro-expressible within the other:
whereas operators would connect forms, functions would transform functions,
the macro-morphism typically consisting in protecting forms with a lambda
to obtain a function.
	Hence,	``E \cup F''	means	"either E or F",
	and	``E \cap F''	means	"both E and F",
which gives us union and intersection (logical) types.

The interesting operator, that made me call the system "reflective",
and allowed for expressing logical statements, is subtypep (written \lhd),
that compares logical types of its two connected subforms,
and expresses intuitionnist implication.
False is modelized as the bottom type of forms that diverge,
True is modelized as the top type of forms that converge toward any value.

Contrarily to usual type systems, that lose so much information,
that you don't know much anything about evaluation of a term,
types herein embody the whole of meaningful information of a term
with respect to evaluation, which is why they correspond to the
model-theoretic notion of "(logical) type". Of course, this
makes static typing undecidable in the general case.

Now doing research for my PhD, I am currently writing a paper on Reflection,
where I intend to reuse this calculus (giving a better-founded formal
semantics for it than I did in my Masters Thesis), and describe how it
can be used as the kernel of a reflective system.

For my bibliography, I'm looking for a paper that already describes
the above calculus, or most likely, just the subset without subtypep.
If such paper already exists, I can just \cite{it}, an not have to worry
anymore about theoretical details; if no such paper exists,
then I get to write one and get the (dis)credit.

Also, papers about general methods to easily formalize such variants of
the lambda-calculus, instead of particular formalized variants,
as well as hints about whom or where (newsgroup, mailing list, real-life, etc)
to ask for help are most welcome.

Thank you for your attention.

PS: In case anyone is interested, my Masters Thesis (in french) should be
available from my web page http://www.tunes.org/~fare/files/:

@MastersThesis{Rideau97,
	Author={Fran{ç}ois-Ren{é} Rideau},
	Title={Système de Preuves pour un Langage Purement Fonctionnel},
	School={{U}niversité de {N}ice},
	Type={Rapport de {DEA}},
	Year={1997}}

## Faré | VN: Уng-Vû Bân   | Join the TUNES project!  http://www.tunes.org/ ##
## FR: François-René Rideau |    TUNES is a Useful, Not Expedient System     ##
## Reflection&Cybernethics  | Project for a Free Reflective Computing System ##
The utterly unspeakable is utterly irrelevant.
		-- Faré