<maayhme>
do you use linear logic or non-commutative or something, in Coq ? Or are you working on gentzen intuitionistic logic
<maayhme>
Id be very interrested to work more on theorem proving
<maayhme>
but Im on a modelchecking project atm
<maayhme>
sorry
<Smerdyakov>
I use the boring general intuitionistic logic ATM.
<Smerdyakov>
And extract it to OCaml programs.
<maayhme>
ah yea, this direction
<maayhme>
still working on TAL as well ?
pango_ has joined #ocaml
<Smerdyakov>
Perhaps again soon. I am starting smaller this time.
<Smerdyakov>
Very simple TALs are in the near future, but not a "realistic" one.
<maayhme>
have you seen curry-howard isomorphism for machine code ?
<maayhme>
some japanese guy
<Smerdyakov>
Oh my goodness.
<maayhme>
proof-directed decompilation
<Smerdyakov>
That sounds like a trip.
<Smerdyakov>
I'm using Curry-Howard to _check_ machine code, but nothing like that. :)
<maayhme>
I remmeber reading another paper of them featuring the "the logical abstract machine"
<Smerdyakov>
I'm hacking on teeny bits of Coq to make it extract more efficient programs.
<Smerdyakov>
Like extract natural numbers to use native integers.
<maayhme>
okay
<Smerdyakov>
Apparently we have spoken before, but I don't remember the nickname you are using now. Was it something else before?
<maayhme>
lambdawar maybe
<maayhme>
you may also not remember me
<maayhme>
simply
<maayhme>
:)
<Smerdyakov>
I usually remember nicks. *shrug*
<maayhme>
so, do you generate pure functional programs Smerdyakov ? or do you use some kind of states
<maayhme>
I guess no state
<Smerdyakov>
I think I'm going to be able to swing it with pure functional programs, and some parameters that are implemented with imperative code.
<maayhme>
'kay
UziMonkey has quit [Remote closed the connection]
<maayhme>
do you think at some point we could use the isomorphism in both direction for a single algorithm, using combinator theory as a glue logic ?
<maayhme>
I never implemented such code, I dont see clearly the advantage of each approach
<Smerdyakov>
Sorry, I don't understand what you are suggesting.
<maayhme>
always worked from programs to proofs in my way of thinking ..
<maayhme>
I mean, using coq for generating programs means using curry-howard from the logic set to the lambda calculus set of programs, right
<Smerdyakov>
Yes, though "logic" _is_ "lambda calculus" in Coq.
<maayhme>
yea, but projects like TAL think about the problem in the inverse way
<Smerdyakov>
I don't see any kind of rigorous characterization there.
<maayhme>
I mean, TAL takes real TAL programs, and try to proof stuff on it, instead of generating a program from its proof
pango has quit [Read error: 110 (Connection timed out)]
<maayhme>
I dont know if there is anything as powerful as curry-howard for TAL, last time I checked one of their paper, I read enough to see they had CPS quite early
<maayhme>
from tal to ...
<Smerdyakov>
System F
<maayhme>
yea, polymorphic lambda calculus
<maayhme>
of girard
<maayhme>
and my point was: maybe mixing both approaches of formal proofs could be interresting
<maayhme>
maybe its just stupid
<maayhme>
;)
<maayhme>
I dont know, I have no theorem proving experience
<maayhme>
any word to add ?
<Smerdyakov>
Nope. :)
<maayhme>
good
<maayhme>
ahah
vezenchio has joined #ocaml
Snark has joined #ocaml
ski has joined #ocaml
ski_ has joined #ocaml
ski has quit [Nick collision from services.]
ski_ is now known as ski
vodka-goo has joined #ocaml
mlh has quit [Client Quit]
Submarine has joined #ocaml
smimou has joined #ocaml
noj has quit ["leaving"]
avlondon1 has joined #ocaml
noj has joined #ocaml
avlondono has quit [Read error: 110 (Connection timed out)]
smimou has quit ["?"]
Snark has quit ["Leaving"]
avlondono has joined #ocaml
pango_ has quit [Remote closed the connection]
avlondon1 has quit [Read error: 110 (Connection timed out)]
pango has joined #ocaml
avlondono has quit [Read error: 113 (No route to host)]
Skal has joined #ocaml
avlondono has joined #ocaml
Submarine has quit ["Leaving"]
<haelix>
06:12 < Smerdyakov> I don't see any kind of rigorous characterization there.
<haelix>
06:13 < maayhme> I mean, TAL takes real TAL programs, and try to proof stuff on
* haelix
is sorry
revision17_ has joined #ocaml
Revision17 has quit [Read error: 110 (Connection timed out)]
m3ga has joined #ocaml
<maayhme>
haelix, yea ? explain
<haakonn_>
he is sorry for accidentally pasting text
haakonn_ is now known as haakonn
avlondono has quit [Read error: 110 (Connection timed out)]
avlondono has joined #ocaml
pango has quit [Remote closed the connection]
m3ga has quit [Read error: 104 (Connection reset by peer)]
m3ga has joined #ocaml
m3ga has quit ["disappearing into the sunset"]
threeve has joined #ocaml
__DL__ has joined #ocaml
chs_ has quit [Read error: 104 (Connection reset by peer)]
chs_ has joined #ocaml
ski has quit [Read error: 110 (Connection timed out)]
chs_ has quit [Remote closed the connection]
chs_ has joined #ocaml
smimou has joined #ocaml
Snark has joined #ocaml
Schmurtz has quit [Read error: 113 (No route to host)]
Schmurtz has joined #ocaml
fluxx has joined #ocaml
fluxx has quit [Client Quit]
mflux has joined #ocaml
tom_p has joined #ocaml
tom_p has quit [Client Quit]
tom_p has joined #ocaml
ski has joined #ocaml
mrsolo has joined #ocaml
tom_p has quit ["Leaving"]
mikeX has joined #ocaml
Boojum has joined #ocaml
mikeX has quit ["Leaving"]
UziMonkey has joined #ocaml
Snark has quit [Read error: 110 (Connection timed out)]
Submarine has joined #ocaml
tom_p has joined #ocaml
Boojum is now known as Snark
UziMonkey has quit [Remote closed the connection]
tom_p has quit ["Leaving"]
Schmurtz has quit [Read error: 110 (Connection timed out)]
pango has joined #ocaml
Msandin has joined #ocaml
Submarine has quit ["Leaving"]
Nutssh has quit ["Client exiting"]
smimou has quit ["?"]
vezenchio has quit ["Free Tibet with each Asian nation of a lesser or equal value"]
Snark has quit ["Leaving"]
chs__ has joined #ocaml
chs_ has quit [Read error: 113 (No route to host)]
Msandin has quit [Read error: 104 (Connection reset by peer)]
Submarine has joined #ocaml
Submarine has quit ["Leaving"]
UziMonkey has joined #ocaml
__DL__ has quit [Remote closed the connection]
Skal has quit [Read error: 54 (Connection reset by peer)]
Skal has joined #ocaml
threeve has quit []
UziMonkey has quit [":q"]
ski has quit ["externalized internal iteration using shift/reset !"]