Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: Proofs as programs
Date: Wed, 18 Dec 2024 16:31:55 +0100
Organization: A noiseless patient Spider
Lines: 19
Message-ID: <vjuptb$1m602$1@dont-email.me>
References: <vjks2t$sghb$1@solani.org> <vjksaq$sgo6$1@solani.org>
 <vjksdb$sgo6$2@solani.org> <vjs63g$1m603$1@dont-email.me>
 <vjsl6t$1dmbi$1@solani.org> <vjt8up$1m603$3@dont-email.me>
 <vjttuv$10v9c$1@solani.org> <vjtueg$10vjo$1@solani.org>
 <vju67k$1m603$4@dont-email.me> <vjulf8$1er6n$1@solani.org>
 <vjumaf$1erpp$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 18 Dec 2024 16:31:57 +0100 (CET)
Injection-Info: dont-email.me; posting-host="ecdb2d4a7a6f6121f563c95811975b2c";
	logging-data="1775618"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19h5pH7PSRQ4WpdzFpdCvbkeb/a31cuaHM="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:N67Lb9c7n1ppohQe6QxsAkQXEdc=
In-Reply-To: <vjumaf$1erpp$1@solani.org>
Content-Language: en-GB
Bytes: 1840

On 18/12/2024 15:30, Mild Shock wrote:

> Maybe your work qualifies for Weekend 3.

In fact, I have replied to the WE3 announcement.

> I don't know yet. You have to tell us. Do
> you think it implements a Natural Deduction
> with Simple Types proof extraction?

It implements "affine intuitionistic propositional logic", and I am 
getting to evaluation/compilation which is the functional side (more 
details in my initial reply): so, sure, I even classify my reduction 
rules as intros vs elims...

What is the deadline?  I don't know what WE is 3.

-Julio