deep inference combinators implementation

Kai Brünnler <[email protected]> Wed, 16 Feb 2011 22:14:54 +0100
Newsgroups gmane.science.mathematics.frogs
Message-ID <[email protected]>
--000e0cd59cd8b32fff049c6cc555
Content-Type: text/plain; charset=ISO-8859-1

Hi Frogs,

as an exercise, I've started implementing a interpreter for a little
programming language based on deep inference (in the Curry-Howard sense).
The implementation is in Scala and is shared here on
GitHub<https://github.com/kaibr/dicomb>.
Take a look if you're interested. It can already do amazing things: you
could execute a program that takes an ordered pair and returns its first
component!

Comments and contributions are welcome, of course! I've just barely started,
so it should be easy to get into. I'm currently in the process of
implementing a parser (yes, right now programs are given as abstract syntax
trees), and then I'd like to add lots of example programs to test the
interpreter and the type inference and to experiment with the language.

Oh yes, the paper it is based on is "An Algorithmic Interpretation of a Deep
Inference System" by Richard and myself, available from
here<http://www.iam.unibe.ch/%7Ekai/Papers/2008aidis.pdf>,
if you'd like some background.

Best wishes and maybe happy hacking!

-Kai

--000e0cd59cd8b32fff049c6cc555
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable

<br>Hi Frogs,<br><br>as an exercise, I&#39;ve started implementing a interp=
reter for a little programming language based on deep inference (in the Cur=
ry-Howard sense). The implementation is in Scala and is shared <a href=3D"h=
ttps://github.com/kaibr/dicomb">here on GitHub</a>. Take a look if you&#39;=
re interested. It can already do amazing things: you could execute a progra=
m that takes an ordered pair and returns its first component!<br>
<br>Comments and contributions are welcome, of course! I&#39;ve just barely=
 started, so it should be easy to get into. I&#39;m currently in the proces=
s of implementing a parser (yes, right now programs are given as abstract s=
yntax trees), and then I&#39;d like to add lots of example programs to test=
 the interpreter and the type inference and to experiment with the language=
.<br>
<br>Oh yes, the paper it is based on is &quot;An Algorithmic Interpretation=
 of a Deep Inference System&quot; by Richard and myself, <a href=3D"http://=
www.iam.unibe.ch/%7Ekai/Papers/2008aidis.pdf">available from here</a>, if y=
ou&#39;d like some background. <br>
<span id=3D"goog_685275130"></span><span id=3D"goog_685275131"></span><br>B=
est wishes and maybe happy hacking!<br><br>-Kai<br><br>

--000e0cd59cd8b32fff049c6cc555--