HOAS Techniques in Verified Transformations on Functional Programs

--===============1927957895==
Content-Type: multipart/alternative; boundary=001a114414a69b830b052c148475

--001a114414a69b830b052c148475
Content-Type: text/plain; charset=UTF-8

[Apologies for multiple postings]
---

    Verified Transformations on Functional Programs Using
           Higher-Order Abstract Syntax Techniques

I would like to announce the work that I have been doing as part
of my doctoral thesis to bring out the benefits of higher-order
abstract syntax methods in implementing and verifying compiler
transformations commonly used for functional programming
languages. Transformations such as closure conversion and code
hoisting have to pay special attention to binding structure, an
aspect that is given a meta-level treatment in systems such as
Abella, Beluga, Twelf and Lambda Prolog. In collaborative work
with Gopalan Nadathur that will be presented at ESOP 2016, we
have shown how the devices present in Lambda Prolog and Abella,
two systems developed collaboratively by our group at the
University of Minnesota and the Parsifal group at Inria-Saclay,
can used to provide succinct implementations and clear formal
proofs for the correctness of these transformations in the
context of a representative functional language. The
implementation, proofs and accompanying paper are available at
the following URL:

http://www-users.cs.umn.edu/~yuting/compilation/index.html

I would appreciate any comments you might have about the code and the
proofs and would also be happy to answer any questions that arise as
you look at the material.

Best,
- Yuting


-- 
Yuting Wang <[email protected]>
University of Minnesota, Dept. of Computer Science
http://www.cs.umn.edu/~yuting

--001a114414a69b830b052c148475
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div><div>[Apologies for multiple postings]<br>---<br><br>=
=C2=A0=C2=A0=C2=A0 Verified Transformations on Functional Programs Using<br=
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 Higher-Order =
Abstract Syntax Techniques<br><br>I would like to announce the work that I =
have been doing as part<br>of my doctoral thesis to bring out the benefits =
of higher-order<br>abstract syntax methods in implementing and verifying co=
mpiler<br>transformations commonly used for functional programming<br>langu=
ages. Transformations such as closure conversion and code<br>hoisting have =
to pay special attention to binding structure, an<br>aspect that is given a=
 meta-level treatment in systems such as<br><span tabindex=3D"-1" id=3D":3n=
7.85" style=3D"" class=3D"">Abella</span>, Beluga, <span tabindex=3D"-1" id=
=3D":3n7.86" style=3D"" class=3D"">Twelf</span> and Lambda <span tabindex=
=3D"-1" id=3D":3n7.87" style=3D"" class=3D"">Prolog</span>. In collaborativ=
e work<br>with <span tabindex=3D"-1" id=3D":3n7.88" style=3D"" class=3D"">G=
opalan</span> <span tabindex=3D"-1" id=3D":3n7.89" style=3D"" class=3D"">Na=
dathur</span> that will be presented at <span tabindex=3D"-1" id=3D":3n7.90=
" style=3D"" class=3D"">ESOP</span> 2016, we<br>have shown how the devices =
present in Lambda <span tabindex=3D"-1" id=3D":3n7.91" style=3D"" class=3D"=
">Prolog</span> and <span tabindex=3D"-1" id=3D":3n7.92" style=3D"" class=
=3D"">Abella</span>,<br>two systems developed collaboratively by our group =
at the<br>University of Minnesota and the Parsifal group at <span tabindex=
=3D"-1" id=3D":3n7.93" style=3D"" class=3D"">Inria</span>-<span tabindex=3D=
"-1" id=3D":3n7.94" style=3D"" class=3D"">Saclay</span>,<br>can used to pro=
vide succinct implementations and clear formal<br>proofs for the correctnes=
s of these transformations in the<br>context of a representative functional=
 language. The<br>implementation, proofs and accompanying paper are availab=
le at<br>the following URL:<br><br><a href=3D"http://www-users.cs.umn.edu/~=
yuting/compilation/index.html">http://www-users.cs.<span tabindex=3D"-1" id=
=3D":3n7.95" style=3D"" class=3D"">umn</span>.<span tabindex=3D"-1" id=3D":=
3n7.96" style=3D"" class=3D"">edu</span>/~<span tabindex=3D"-1" id=3D":3n7.=
97" style=3D"" class=3D"">yuting</span>/compilation/index.html</a><br><br>I=
 would appreciate any comments you might have about the code and the<br>pro=
ofs and would also be happy to answer any questions that arise as<br>you lo=
ok at the material. <br><br></div>Best,<br></div>- <span tabindex=3D"-1" id=
=3D":3n7.98" style=3D"" class=3D"">Yuting</span><br><br clear=3D"all"><br>-=
- <br><div class=3D"gmail_signature"><div dir=3D"ltr"><div><span tabindex=
=3D"-1" id=3D":3n7.99" style=3D"" class=3D"">Yuting</span> Wang &lt;<a href=
=3D"mailto:[email protected]" target=3D"_blank"><span tabindex=3D"-1" id=3D=
":3n7.100" style=3D"" class=3D"">yuting</span>@cs.<span tabindex=3D"-1" id=
=3D":3n7.101" style=3D"" class=3D"">umn</span>.<span tabindex=3D"-1" id=3D"=
:3n7.102" style=3D"" class=3D"">edu</span></a>&gt;<br></div><div>University=
 of Minnesota, Dept. of Computer Science<br></div><div><a href=3D"http://ww=
w.cs.umn.edu/~yuting" target=3D"_blank">http://www.cs.<span tabindex=3D"-1"=
 id=3D":3n7.103" style=3D"" class=3D"">umn</span>.<span tabindex=3D"-1" id=
=3D":3n7.104" style=3D"" class=3D"">edu</span>/~<span tabindex=3D"-1" id=3D=
":3n7.105" style=3D"" class=3D"">yuting</span></a><br></div></div></div></d=
iv>

--001a114414a69b830b052c148475--

--===============1927957895==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

_______________________________________________
Lprolog mailing list
[email protected]
https://wwws.cs.umn.edu/mm-cs/listinfo/lprolog
--===============1927957895==--