Programming Language
Isabelle Appeared 1986
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).
Trends languish rank #200 languish — 53 periods, 2009Q2 to 2025Q2 2009Q2 2025Q2
Influence graph Influence graph for Isabelle: 28 influencing languages, 0 family links C++ influenced Ada Eiffel influenced Ada Pascal influenced Ada C influenced AWK sed influenced AWK Fortran influenced BASIC Fortran influenced C Ada influenced C++ APL influenced C++ C influenced C++ F# influenced C++ Haskell influenced Clean Haskell influenced CoffeeScript JavaScript influenced CoffeeScript Perl influenced CoffeeScript Python influenced CoffeeScript Ruby influenced CoffeeScript Ada influenced Eiffel Haskell influenced F# Python influenced F# Standard ML influenced F# Clean influenced Haskell Lisp influenced Haskell R5RS influenced Haskell Raku influenced Haskell Scheme influenced Haskell Standard ML influenced Haskell Haskell influenced Isabelle C++ influenced Java AWK influenced JavaScript C influenced JavaScript Java influenced JavaScript Lisp influenced JavaScript Lua influenced JavaScript MoonScript influenced JavaScript Perl influenced JavaScript Python influenced JavaScript R5RS influenced JavaScript Scheme influenced JavaScript Self influenced JavaScript AWK influenced Lua C influenced Lua C++ influenced Lua Lisp influenced Lua R5RS influenced Lua Scheme influenced Lua Self influenced Lua C++ influenced MoonScript CoffeeScript influenced MoonScript Lua influenced MoonScript Scheme influenced MoonScript AWK influenced Perl BASIC influenced Perl C influenced Perl C++ influenced Perl Lisp influenced Perl Raku influenced Perl sed influenced Perl Ada influenced Python APL influenced Python C influenced Python C++ influenced Python Haskell influenced Python Lisp influenced Python Perl influenced Python R5RS influenced Python Scheme influenced Python Standard ML influenced Python Lisp influenced R5RS Haskell influenced Raku JavaScript influenced Raku Perl influenced Raku Ruby influenced Raku BASIC influenced Ruby C++ influenced Ruby Eiffel influenced Ruby Lisp influenced Ruby Lua influenced Ruby MoonScript influenced Ruby Perl influenced Ruby Python influenced Ruby R5RS influenced Ruby Scheme influenced Ruby Smalltalk influenced Ruby Lisp influenced Scheme APL influenced Self Pascal influenced Standard ML Fortran sed C Pascal Eiffel BASIC Lisp AWK Ada Standard ML APL Perl R5RS Scheme Python F# C++ Self Lua Smalltalk Ruby CoffeeScript Java MoonScript JavaScript Raku Clean Haskell Isabelle Solid arrows: influence, oldest at the top. Dashed: compiles to / is a dialect of / implements. 