Re: Proofs as programs

Sujet : Re: Proofs as programs
De : julio (at) *nospam* diegidio.name (Julio Di Egidio)
Groupes : sci.logic
Date : 22. Dec 2024, 18:13:04

Autres entêtes

Organisation : A noiseless patient Spider
Message-ID : <vk9hb1$innf$2@dont-email.me>
References : 1 2 3 4 5
User-Agent : Mozilla Thunderbird

On 19/12/2024 18:40, Julio Di Egidio wrote:

My interpretation might be unorthodox, anyway here is concretely what I am doing (a far better approximation that is): <https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Syntax-directed_rule_system>

That is, Hindley-Milner upside down:
a *closed* universe with Prop on top...
-Julio

Date	Sujet	#	Auteur
14 Dec 24	Advent of Logic 2024: Weekend 1	58	Mild Shock
14 Dec 24	Advent of Logic 2024: Weekend 2 (Was: Advent of Logic 2024: Weekend 1)	36	Mild Shock
14 Dec 24	Re: Advent of Logic 2024: Weekend 3 (Was: Advent of Logic 2024: Weekend 2)	35	Mild Shock
17 Dec 24	Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	33	Julio Di Egidio
17 Dec 24	Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	1	Julio Di Egidio
17 Dec 24	Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	21	Mild Shock
17 Dec 24	Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	3	Mild Shock
17 Dec 24	Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	1	Mild Shock
17 Dec 24	Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	1	Mild Shock
18 Dec 24	Re: Proofs as programs	17	Julio Di Egidio
18 Dec 24	Re: Proofs as programs	16	Mild Shock
18 Dec 24	Re: Proofs as programs	15	Mild Shock
18 Dec 24	Re: Proofs as programs	14	Julio Di Egidio
18 Dec 24	Re: Proofs as programs	13	Mild Shock
18 Dec 24	Hilbert Style proof system (Was: Proofs as programs)	12	Mild Shock
18 Dec 24	Re: Proofs as programs	11	Julio Di Egidio
19 Dec 24	What are Simple Types (Was: Proofs as programs)	10	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	2	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	1	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	7	Julio Di Egidio
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	6	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	2	Julio Di Egidio
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	1	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	3	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	1	Mild Shock
19 Dec 24	Re: What are Simple Types (Was: Proofs as programs)	1	Julio Di Egidio
19 Dec 24	Re: Proofs as programs (Was: Advent of Logic 2024: Weekend 3)	5	Julio Di Egidio
22 Dec 24	Re: Proofs as programs	4	Julio Di Egidio
23 Dec 24	/* A / and / B */ are different (Was: Proofs as programs)	3	Mild Shock
23 Dec 24	The Task is called the Inhabitation Problem (Was: /* A / and / B */ are different)	1	Mild Shock
23 Dec 24	Re: /* A / and / B */ are different (Was: Proofs as programs)	1	Julio Di Egidio
21 Dec 24	Curry-Howard Correspondence where? (Was: Proofs as programs (Was: Advent of Logic 2024: Weekend 3))	5	Mild Shock
21 Dec 24	A Christmas Miracle (Was: Curry-Howard Correspondence where?)	4	Mild Shock
21 Dec 24	Re: A Christmas Miracle (Was: Curry-Howard Correspondence where?)	3	Mild Shock
21 Dec 24	Re: A Christmas Miracle (Was: Curry-Howard Correspondence where?)	2	Mild Shock
21 Dec 24	Re: A Christmas Miracle (Was: Curry-Howard Correspondence where?)	1	Mild Shock
27 Dec 24	4th Family Member: Relevant Logic (Re: Advent of Logic 2024: Weekend 3)	1	Mild Shock
20 Dec 24	Advent of Logic 2024: Specification and Deadline (Was: Advent of Logic 2024: Weekend 1)	20	Mild Shock
20 Dec 24	Re: Advent of Logic 2024: Specification and Deadline (Was: Advent of Logic 2024: Weekend 1)	15	Mild Shock
20 Dec 24	Advent of Logic 2024: Solution Weekend 2 (Was: Advent of Logic 2024: Specification and Deadline)	1	Mild Shock
20 Dec 24	Repetition vs Use (Was: Advent of Logic 2024: Specification and Deadline)	13	Julio Di Egidio
20 Dec 24	Re: Repetition vs Use (Was: Advent of Logic 2024: Specification and Deadline)	12	Mild Shock
20 Dec 24	Re: Repetition vs Use (Was: Advent of Logic 2024: Specification and Deadline)	11	Julio Di Egidio
20 Dec 24	Please be patient (Was: Repetition vs Use)	10	Mild Shock
20 Dec 24	Happy Now? (Was: Please be patient)	9	Mild Shock
20 Dec 24	Re: Happy Now? (Was: Please be patient)	8	Julio Di Egidio
21 Dec 24	What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	7	Mild Shock
21 Dec 24	Re: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	6	Julio Di Egidio
21 Dec 24	Re: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	5	Mild Shock
21 Dec 24	Re: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	1	Mild Shock
21 Dec 24	Re: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	3	Julio Di Egidio
21 Dec 24	Re: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	2	Mild Shock
21 Dec 24	Re: What is it, a Bird or an Airplane? (Was: Happy Now? (Was: Please be patient))	1	Julio Di Egidio
21 Dec 24	Advent of Logic 2024: Friendly Reminder (Re: Advent of Logic 2024: Specification and Deadline)	4	Mild Shock
24 Dec 24	Re: Advent of Logic 2024: Friendly Reminder (Re: Advent of Logic 2024: Specification and Deadline)	3	Mild Shock
24 Dec 24	Linear Logic as Natural Deduction (Was: Advent of Logic 2024: Friendly Reminder)	2	Mild Shock
24 Dec 24	Re: Linear Logic as Natural Deduction (Was: Advent of Logic 2024: Friendly Reminder)	1	Mild Shock
17 Jan 25	Combinatorial Simple Typed Solution (Re: Advent of Logic 2024: Weekend 1)	1	Mild Shock

Haut de la page

Les messages affichés proviennent d'usenet.

NewsPortal