Kenneth Udut ok, I wasn’t nuts: I knew _somebody_ had to see what I saw: There’s a Linear Chemical Abstract Machine calculus which is a calculus based upon the physics of chemical diffusion, abstracted into a parallel processing computing logic basically. But BECAUSE it’s a computing logic, it can be transformed into Linear Logic via the Curry Howard isomorphism. So because Jean-Yves Girard embedded Intuitionistic Logic into Linear Logic. typed Lambda calculus is therefore embedded into Linear Chemical Abstract Machine. The Kinetics:intuitionistic logic “Introduction Abramsky’s Linear Chemical Abstract Machine is a term calculus which corresponds to Linear Logic, via the Curry-Howard isomorphism. We show that the typed λ-calculus is embedded into Linear Chemical Abstract Machine by Girard’s embedding of Intuitionistic Logic into Linear Logic. Then we extend our result to a simple functional programming language obtained from the typed λ-calculus by adding constants from PCF. We show that the call-by-value evaluation of terms of ground types (Booleans and Natural numbers) are preserved and reflected by this translation. Finally, we discuss an operational perspective of our result. We give a sequential execution model of Linear CHAM based on Abramsky’s idea of a stack of coequations and a name queue, and then we consider a concurrent multi-thread implementation of the model.” “Conclusion: We have shown that the typed lambda-calculus is embedded into Linear CHAM by Girard’s embedding of Intuitionistic Logic into Linear Logic. In addition, we have extended this result to a simple functional programming language with constants. Finally, we have introduced sequential and concurrent execution models of Linear CHAM. From these results, we can expect that Linear CHAM can be used as a foundation of concurrent functional languages with types.” https://shibaura.pure.elsevier.com/en/publications/an-implementation-model-of-the-typed-λ-calculus-based-on-linear-c

Kenneth Udut

ok, I wasn’t nuts: I knew _somebody_ had to see what I saw:
There’s a Linear Chemical Abstract Machine calculus which is a calculus based upon the physics of chemical diffusion, abstracted into a parallel processing computing logic basically.
But BECAUSE it’s a computing logic, it can be transformed into Linear Logic via the Curry Howard isomorphism.
So because Jean-Yves Girard embedded Intuitionistic Logic into Linear Logic. typed Lambda calculus is therefore embedded into Linear Chemical Abstract Machine.
The Kinetics:intuitionistic logic
“Introduction
Abramsky’s Linear Chemical Abstract Machine is a term calculus which corresponds to Linear Logic, via the Curry-Howard isomorphism. We show that the typed λ-calculus is embedded into Linear Chemical Abstract Machine by Girard’s embedding of Intuitionistic Logic into Linear Logic. Then we extend our result to a simple functional programming language obtained from the typed λ-calculus by adding constants from PCF. We show that the call-by-value evaluation of terms of ground types (Booleans and Natural numbers) are preserved and reflected by this translation. Finally, we discuss an operational perspective of our result. We give a sequential execution model of Linear CHAM based on Abramsky’s idea of a stack of coequations and a name queue, and then we consider a concurrent multi-thread implementation of the model.”
“Conclusion:
We have shown that the typed lambda-calculus is embedded into Linear CHAM by Girard’s embedding of Intuitionistic Logic into Linear Logic. In addition, we have extended this result to a simple functional programming language with constants. Finally, we have introduced sequential and concurrent execution models of Linear CHAM. From these results, we can expect that Linear CHAM can be used as a foundation of concurrent functional languages with types.”

Leave a comment

Your email address will not be published. Required fields are marked *


+ nine = 16

Leave a Reply