---
key: pl/isabelle
kind: plang
name: "Isabelle"
url: https://plangs.page/isabelle
---

# Isabelle

> Automated theorem prover for formalizing mathematical proofs in higher-order logic.

Automated theorem prover that allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. It is written in Standard ML and Scala, supporting both procedural and declarative proof styles. Isabelle is designed to be a flexible IDE for formal methods and supports a wide variety of formal proofs and methods, notably higher-order logic (HOL).

## Facts

- Appeared: 1986
- Homepage: https://isabelle.in.tum.de/
- Languish ranking: #200

## Relationships

### Paradigms

- [Declarative](https://plangs.page/paradigm/declarative)
- [DSL](https://plangs.page/paradigm/dsl)
- [Logic](https://plangs.page/paradigm/logic)

### Platforms

- [Apple](https://plangs.page/platform/apple)
- [Linux](https://plangs.page/platform/linux)
- [Windows](https://plangs.page/platform/windows)

### Type Systems

- [Algebraic Data Types](https://plangs.page/type-system/algebraic)
- [Dependent](https://plangs.page/type-system/dependent)
- [Static](https://plangs.page/type-system/static)
- [Strong](https://plangs.page/type-system/strong)

### Influenced By

- [Haskell](https://plangs.page/haskell)

### Written With

- [Scala](https://plangs.page/scala)
- [Standard ML](https://plangs.page/standard-ml)

### Licenses

- [BSD](https://plangs.page/license/bsd)

### Tags

- [Application Framework](https://plangs.page/tag/framework)
- [Automation](https://plangs.page/tag/automation)
- [Control](https://plangs.page/tag/control)
- [Industrial Control](https://plangs.page/tag/industrial)
- [Interpreter](https://plangs.page/tag/interpreters)
- [Mathematical Modeling](https://plangs.page/tag/modeling)
- [Proof Assistant](https://plangs.page/tag/proofs)
- [Wavelet](https://plangs.page/tag/wavelet)