René Thiemann

 

Website: http://cl-informatik.uibk.ac.at/~thiemann/

 

Entries

2020

May 13: A Formalization of Knuth–Bendix Orders

 

2019

June 21: Linear Inequalities

January 17: Farkas' Lemma and Motzkin's Transposition Theorem

 

2018

August 24: An Incremental Simplex Algorithm with Unsatisfiable Core Generation

February 6: First-Order Terms

February 6: A verified factorization algorithm for integer polynomials with polynomial complexity

February 2: A verified LLL algorithm

 

2017

November 22: Stochastic Matrices and the Perron-Frobenius Theorem

April 6: Subresultants

 

2016

October 14: The Factorization Algorithm of Berlekamp and Zassenhaus

May 20: Perron-Frobenius Theorem for Spectral Radius Analysis

January 29: Polynomial Interpolation

January 29: Polynomial Factorization

 

2015

December 22: Algebraic Numbers in Isabelle/HOL

August 21: Matrices, Jordan Normal Forms, and Spectral Radius Theory

March 11: Deriving class instances for datatypes

 

2014

October 13: Lifting Definition Option

October 3: XML

October 3: Certification Monads

July 29: Haskell's Show Class in Isabelle/HOL

February 18: Mutually Recursive Partial Functions

February 6: Implementing field extensions of the form Q[sqrt(b)]

 

2013

January 3: Computing N-th Roots using the Babylonian Method

 

2012

August 7: Generating linear orders for datatypes

February 29: Executable Transitive Closures

 

2011

March 14: Executable Transitive Closures of Finite Relations

 

2010

August 10: Executable Multivariate Polynomials

June 17: Executable Matrix Operations on Matrices of Arbitrary Dimensions

June 14: Abstract Rewriting