https://github.com/groupoid/anders
Anders is HoTT theorem prover based on: classical MLTT-80 with 0, 1, 2, W types; CCHM in CHM flavour as cubical type system with hcomp/trans Kan operations; HTS sctrict equality on pretypes; de Rham stack modality primitives. We tend not to touch general recursive higher inductive schemes yet, instead we will try to express as much HIT as possible through W, Coequlizer and HubSpokes Disc in the...
* You can use both Erlang DSL and/or DTL templates
* You can use JSON, BERT, RAW BINARY messages. see http://synrc.com/apps/n2o/doc/web/protocol.htm
* You can use N2O both as server-render and in SPA mode
Proposal
The First Erlang PaaS with LXC and Xen Erlang applications and dev environment. Prives basic application bones for Blog, App Store and Social network full-stack Erlang applications.
Provides High-Level Access to Acl, Users, Groups, Subscriptions, Feeds, Comments, Meetings, Accounts, Payments, Products, Purchases, etc.