Andreas (Andy) Schropp

schropp (a)

I finished my computer science degree at TUM in 2012. From 2012 to early 2014 I was working at COMSA GmbH, helping improve processes around the construction of automotive wiring harnesses.

I am currently investigating the large-scale use of meta-computational principles, in particular towards advancements in the mechanization of mathematics.

This page is dedicated to collect the academic results.

Research Interests

I am interested in automated and interactive theorem proving, machine learning, logic, programming languages, {set, category, type} theory and related fields.

The Isabelle theorem prover is my favorite vehicle for research in applied logic. I am often involved in projects with people of the Chair for Logic and Verification, headed by Tobias Nipkow.

The following subtopics have a special place in my life:



Andreas Schropp and Andrei Popescu. Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory. CPP 2013.
   Moved to new GitHub repository.
   Download referenced CPP2013 bundle.

Alexander Krauss and Andreas Schropp. A Mechanized Translation from Higher-Order Logic to Set Theory. ITP 2010.

Master Thesis (Diplomarbeit)

Andreas Schropp. Instantiating deeply embedded many-sorted theories into HOL types in Isabelle. Technische Universität München 2012.

Tools towards a Vision

I have implemented various tools for the Isabelle Theorem Prover which serve to explore the practical aspects of my ideas: