Arend

A dependently typed language based on homotopy type theory (HoTT) and Cubical type theory.

This is developed by jetbrains (more about jetbrains on page here).

https://arend-lang.github.io/

Installation

First install Jetbrains as discussed on page here.

Then, in the plugins page, search for 'arend' and click on install:

plugin page screenshot

Restart Jetbrains to use the plugin.

metadata block
see also:

 
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Executable UML - Covers compiler issues but no code
cover Executable UML - concentrates on patterns

cover Fast Track UML 2.0 - useful for people who know some UML but are upgrading to 2.0

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.