LEAN FORMALIZATION OF INSERTION SORT STABILITY AND CORRECTNESS
We present a fully mechanized proof of correctness and stability of the insertion sort algorithm, while handling stability not as an afterthought in its formal specification, but rather as a property removing any unspecified behaviour from the algorithm, by explaining what happens to elements that...
Main Authors: | František SILVÁŠI, Martin TOMÁŠEK |
---|---|
Format: | Article |
Language: | English |
Published: |
Sciendo
2018-02-01
|
Series: | Acta Electrotechnica et Informatica |
Online Access: | http://www.aei.tuke.sk/papers/2018/2/06_Silvasi.pdf |
Similar Items
-
EXTENDING LEAN CELLULAR AUTOMATA FRAMEWORK – BOUNDARY CONDITIONS AND PROPERTIES OF CANONICAL FORMS
by: Frantisek SILVASI, et al.
Published: (2020-05-01) -
Formalizing mathematics in LEAN
by: Liu, Yufei
Published: (2024) -
Expressivity of Lean Formalisms
by: Pulman, S
Published: (1994) -
Expressivity of Lean Formalisms
by: Pulman, S
Published: (1994) -
Expressivity of Lean Formalisms
by: Pulman, S
Published: (1994)