Isabelle Alternatives

Isabelle is described as 'Proof assistant for writing and checking mathematical proofs by computer' and is an app in the education & reference category. There are three alternatives to Isabelle for Mac, Windows, Linux and Web-based. The best Isabelle alternative is F*, which is both free and Open Source. Other great apps like Isabelle are Coq and Agda.

  • FreeOpen Source
  • ...

Isabelle is a proof assistant for writing and checking mathematical proofs by computer.

More about Isabelle
Isabelle alternatives page was last updated Feb 22, 2018
Copy a direct link to this comment to your clipboard
  1. F* icon
     3 likes
    Copy a direct link to this comment to your clipboard

    F* is an ML-like functional programming language aimed at program verification. F* can express precise specifications for programs, including functional correctness properties. Programs written in F* can be translated to OCaml or F# for execution.

    6 F* alternatives

    License model

    • FreeOpen Source

    Application type

    Platforms

    • Mac
    • Windows
    • Linux
    • Online

    F* Features

    1.  Portable

    F* VS Isabelle

     
    • F* is the most popular Web-based, Windows, Mac & Linux alternative to Isabelle.

    • F* is the most popular Open Source & free alternative to Isabelle.

    • F* is Free and Open SourceIsabelle is also Free and Open Source
  2. Coq icon
     4 likes
    Copy a direct link to this comment to your clipboard

    Coq is a proof assistant, which allows you to write mathematical proofs in a rigorous and formal way, and have them checked for correctness by the computer. It also allows programming with proofs of correctness for the code, and dependent types.

    License model

    • FreeOpen Source

    Country of Origin

    • International

    Platforms

    • Mac
    • Windows
    • Linux

    Coq VS Isabelle

     
  3. Agda icon
     2 likes
    Copy a direct link to this comment to your clipboard

    Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs...

    License model

    • FreeOpen Source

    Application type

    Platforms

    • Mac
    • Windows
    • Linux

    Agda VS Isabelle

     
3 of 3 Isabelle alternatives