Tools

Without Loss of Generality

by Dominique Unruh

Aug 30

With-Type – Poor man's dependent types

by Dominique Unruh

Aug 29

AutoCorres2

by Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch and Simon Wimmer

Apr 17

Go Code Generation for Isabelle

by Terru Stübinger and Lars Hupel

Jan 22

Unification Utilities for Isabelle/ML

by Kevin Kappelmann

Sep 19

Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

Dec 05

Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML

by Achim D. Brucker

Jul 29

IDE: Introduction, Destruction, Elimination

by Mihails Milehins

Sep 06

Extension of Types-To-Sets

by Mihails Milehins

Sep 06

Conditional Transfer Rule

by Mihails Milehins

Sep 06

Conditional Simplification

by Mihails Milehins

Sep 06

SpecCheck - Specification-Based Testing for Isabelle/ML

by Kevin Kappelmann, Lukas Bulwahn and Sebastian Willenbrink

Jul 01

Automated Stateful Protocol Verification

by Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull

Apr 08

Isabelle/C

by Frédéric Tuong and Burkhart Wolff

Oct 22

Auto2 Prover

by Bohua Zhan

Nov 20

Bounded Natural Functors with Covariance and Contravariance

by Andreas Lochbihler and Joshua Schneider

Apr 24

Operations on Bounded Natural Functors

by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

Dec 19

Homogeneous Linear Diophantine Equations

by Florian Messner, Julian Parsert, Jonas Schöpf and Christian Sternagel

Oct 14

Dictionary Construction

by Lars Hupel

May 24

Monad normalisation

by Joshua Schneider, Manuel Eberl and Andreas Lochbihler

May 05

Constructor Functions

by Lars Hupel

Apr 19

Lazifying case constants

by Lars Hupel

Apr 18

Proof Strategy Language

by Yutaka Nagashima

Dec 20

Separata: Isabelle tactics for Separation Algebra

by Zhe Hou, David Sanan, Alwen Tiu, Rajeev Gore and Ranald Clouston

Nov 16

Generating Cases from Labeled Subgoals

by Lars Noschinski

Jul 21

Nominal 2

by Christian Urban, Stefan Berghofer and Cezary Kaliszyk

Feb 21

A Fast SAT Solver for Isabelle in Standard ML

by Armin Heller

Dec 09

Tools

2024

Without Loss of Generality

With-Type – Poor man's dependent types

AutoCorres2

Go Code Generation for Isabelle

2023

Unification Utilities for Isabelle/ML

2022

Automation of Boolos' Curious Inference in Isabelle/HOL

Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML

2021

IDE: Introduction, Destruction, Elimination

Extension of Types-To-Sets

Conditional Transfer Rule

Conditional Simplification

SpecCheck - Specification-Based Testing for Isabelle/ML

2020

Automated Stateful Protocol Verification

2019

Isabelle/C

2018

Auto2 Prover

Bounded Natural Functors with Covariance and Contravariance

2017

Operations on Bounded Natural Functors

Homogeneous Linear Diophantine Equations

Dictionary Construction

Monad normalisation

Constructor Functions

Lazifying case constants

2016

Proof Strategy Language

Separata: Isabelle tactics for Separation Algebra

2015

Generating Cases from Labeled Subgoals

2013

Nominal 2

2009

A Fast SAT Solver for Isabelle in Standard ML