coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Danil Annenkov <danil.v.annenkov AT gmail.com>
- To: coq-club AT inria.fr, coq+announcements AT discoursemail.com
- Subject: [Coq-Club] Certified Elm web apps
- Date: Mon, 12 Apr 2021 16:29:08 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=danil.v.annenkov AT gmail.com; spf=Pass smtp.mailfrom=danil.v.annenkov AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f171.google.com
- Ironport-hdrordr: A9a23:qlvWWatdidJOc+2Cdids+lbJ7skCWoQji2hD6mlwRA09T+Wxncqjhele8BfyhioYVn1Io6HlBICrR3TA+ZlppawYOrm/VAfr0VHYS71Kx43k3jHmBmnC5vdQvJ0QB5RWJdXsATFB7frSzxK/F78breWv0KftvuvGymcocAcCUdAE0y5cKiK2VnJ7XxNHA51RLuvq2uNiqyC7cXoaKuSXb0N1PNTrnNHAmJL4bRNuPXdOg2OzpAil57LgHx+T0g12aUIs/Z4Z7WPHnwblj5/Nj9iHywTR32KWz5NalMqJ8Lp+LfGMkcQcJ3HQjB+pbu1aNYGqgTZdmo2SwWdvtOOJjwYrPsx15X+UVHqyuwHVwAXl0Cwj8TvL1UKYqWGLm724eBsKT+56wa5JeBrQ7EQt+Ptm1rhQ5nmUs5pMAQmFtDjh5vzFXRBjkUqvpRMZ4K0upk0adbFbRK5arIQZ8k8QOowHBjjC84wiEPNjFoX1+OtWS1WHdHrU11MfguCEbzAWJFOrU0ICssua33x9h3Zi1XICyMgehHsbsLkWYfB/lqL5G5UtsIsLYt4dbKp7CutEa9CwEHb1Wh7JMHifOxDcPoRvAQOIl7fHpJEOoM26cp0By5U/3L7bVklDjHU/f0L1BdfL4YZC9QrVRn6hYC/kxc5f7aVoo7GUfsuvDQSzDHQV1+ewqfQWBcPWH9ypPohNOuTuKWv1FZwM1wriW4NKIX1bSsccvdw8XE+Ds9+jEPywisXrNNLoYJb9GzctXW3yRlEZWiLoHd5N6kCwVmW9hBTKQXvidlb44Yl7HMHhjq8u4blIErcJnhkeiFy/6M3OAyZFqLYOZ0d7IKnqiOe8vmm5/WHB6m9tOhZbE0ZN6LjsSH9Rv2YxQhrJWIdGn+/aVXFZ3XOBKBM6ZdjRChRnvFhy+bi6NdiI3iYpB8i8Pm/fhGtWp3SXVJAVn62F667eC8kFJ6djfJY0ORTAFhRzlwovgnxEchU8XUPaFinjk+G5l5QSHvjYbMRgmw+lLs5ftGLHuSyn1JkSb0peewTrfd+cgA4oSTYRrEZ26bUjjL2JnivqAXcjgcwjWWc8IVi/MfZjNkCodY9UkrfkdEVbVmGRnwGXjBk1Zy7D61gSvGr8NieZEMu7SmZ1izR96OLH4Vl0fmKScwZbcXZhq7BwEmzApzJV3fKUYLGwl0+ccEELzO1YEDytW0pYHipeg/SMkDKFkjeLEnsrgr80OPbGMbgle7bPnny3LomFkrwHAu9U8J5pOMuGiJ5HbcuvPyuuaB/oAeIg3AKY4lw/PjNvlXUimfT0nB3phVLIkEIXML73GhBLVrsbK9aT4yzPXPCTyqh0itozoK+1OmX1YdiW1LHPY1d4W1zuiF/za9tthYFfvKo0urc2NYLcSyH02HZO2wh7Ktz1mkMYSKFy+6vAJYdrYswXd0tijxAUveXKCHFunh39A+c4c11opWTcJcm1773BrqdqHleMvxLqOV6U8zRU+vDMWyfr789VN4sAZUBtLGQs4nVr++2PM7DKAAKxbudZ4R6RKXmmaoJQT6CDBJQdpht3+MuzgueSbib0sTqg/AdTE+ZrySKHSdn3KB+QEeRImubKX2iks++P2oqPqxvZDRG8cF8VgIVZc1d4VLU7thASyKst3CC0Sr/+v0IilHpT6TxqjUTVwYS97HzFEUwuC3yFvrxmGR9JMnaJiszZ9/O/z3qV2kky5bDKCFpQctZSG9IZU4jwKGN0JdINuaOzlpBf+hhrcVMgCXUxhyv62P4j1bCl2O/KU+mnEnvwP0kdkAQ1dLJcj2gvpCVYaM614Yimbgh/LJ92P9IvooRXmilusF798hkVaAhsrBUh0uj2XyzaFmU5Eajlho3thhcE4KCE9l11vX1V3leqkkuVtVSwn8G7vRMP3h7ghx4irb/YSCo6gS5fuAIiyat9MmCVWWqpRX+eKlv4wKYhJHUNMxFb98w7yB7Ya6UbnJG3yGRp6SkhCi8r2rexCyLRTy6RGdCYFkHVKP2lRNppJ/BfNWoIIyToaFDKmpEsQgnJf9kk3BO2gXsKDbWPPKTjYA/1NuhxwIUAf6j3B4iZjoPS0wIc8XcYpYfyk2aEk/Jn9tnzHH8MjfstN6xyfh639yJ52MaJVQ3BP4IL8DjYxlaRkxhwNZsT2UAJ2kEUqicbBTOwC96yTk9noiQay5WBflxl9e+RDdBPsWnApla9uH7ZcACMWXPcIIEw3w==
- Ironport-phdr: A9a23:w0hPgRI47LhRWttQktmcuERhWUAX047cDksu8pMizoh2WeGdxfzKAkXT6L1XgUPTWs2DsrQY0ruQ6vC/EjdYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba52IRmssAnctcsbjYRsJ6ot1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2hqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TzqUEBrR2/BQmoGeji1jlIhnno0q080OQhFh/G1xEnEt0TqnvUqtT1NKMIXeCr1qXH1zPDb/VI1jf764jIdQ4hrOqDXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkCvGaH9eRvT/6vi3I5pAFrpDii3skihpTUio8I1l3J6SR0zok6KNC6VEJ2Y8OpHZlTui+UNoZ7TN0vT311tSon1LELuZy2cSsUxJonyRPSZP2Kf5WO7xn+WuiRJjJ4i2hkeLK5nxuy/kmgyvH8Vsmpy1lGtDZKkt7JtnwVyRPT7syHSvpj8Uu4wzmPzxjT5vtYLkAzkKrXM4MuzaQ2lpoVr0vDGCz2mELojKOMc0Ur5O6l4PnkbLX+vpKQKZN4hwXkPqktmsGzG/o0PhQNUmSB5Oix1qDv8EvkS7tQlPI2iLPWsJXCKMQbuKG5BwhV354m6xmlDjem1M0UnX0FLF5YYR6HgZXlNlPTLPziAve/hFOskDhvx//YJLHuHpLNLn3bnLfge7Zy9VJcxRItwdxD459YELIMLfLpVkPvqNDVDQU1PxG2zur6ENl905kRWWOLAq+XKqPStlqI6/oyLOaWYo8VuTL9J+I75/L0l3A5n1kdcrev3ZsUb3C4AO9rI0qcYXX2g9cBFX0GsRY5TOzvkFGCSyJcZ26uX6Ig4TE2EJ6pDYDaRoy0nLOB2Dq7EYZNa2BdClGMFG/oeJ+eV/cNbiKSOM5hnSYeWbivUY9ynS2p4QT90v9sKvfe0iwer5PqktZvo6XYkghx/DpyCNmb2GyIQmdohUsERiQ9271lukF4w1aHl6N/hq92D9tWst9AVAY+fbfayeF8CNfsElbNd9GITBC4BNygBzw3TdUv69ALakd5Xd6li0aQjGKRH7YJmunTV9QP+aXG0i2pT+5Njk3e3axktGEIB9NVPAWOiat29gyVDInMwR3xv5bvTrwV2Wv2zEnGzWeKuylwVQdxVeDBXylaaBKJ9JL24UTNS7LoArMiYFMp4f7HEbNDb5jStXsDQf7iPNrEZGfZs2i1DBeMgLiLadizE1g=
Dear Coq community,
I would like to share a project related to the Elm functional programming language.
As part of ConCert (https://github.com/AU-COBRA/ConCert), we have developed an extraction pipeline that allows for generating Elm code.
We have several simple examples/tests here https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmExtractExamples.v.
A more "domain-specific" example with a web app consisting of an input form, validation and rendering a list of users is available here:
https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmForms.v
The example is inspired by a similar one from the Elm guide.
We use Coq's subset types to encode the invariants for the part of the model that represents valid data.
Currently, we write the "logic" of the app (model and validation) in Coq, extract it and then concatenate with the hand-written view, that renders the form and calls the model functions.
Here is the result of the extraction in the online IDE Ellie:
https://ellie-app.com/cSFtmjq99Rta1
Contributions with more interesting examples are very welcome!
--
I would like to share a project related to the Elm functional programming language.
As part of ConCert (https://github.com/AU-COBRA/ConCert), we have developed an extraction pipeline that allows for generating Elm code.
We have several simple examples/tests here https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmExtractExamples.v.
A more "domain-specific" example with a web app consisting of an input form, validation and rendering a list of users is available here:
https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmForms.v
The example is inspired by a similar one from the Elm guide.
We use Coq's subset types to encode the invariants for the part of the model that represents valid data.
Currently, we write the "logic" of the app (model and validation) in Coq, extract it and then concatenate with the hand-written view, that renders the form and calls the model functions.
Here is the result of the extraction in the online IDE Ellie:
https://ellie-app.com/cSFtmjq99Rta1
Contributions with more interesting examples are very welcome!
--
- [Coq-Club] Certified Elm web apps, Danil Annenkov, 04/12/2021
Archive powered by MHonArc 2.6.19+.