schropp in.tum.de

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.

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:

- imposing intensional structure and type-theoretic reasoning on set theory
- configurable dependent type inference
- realizing construction principles ("packages" in HOL parlance) by animating their formalized meta-theories with a general infrastructure, in the hope to speed-up, improve and democratize formal logic implementation efforts
- approximating mathematical structuralism, particularly via isomorphic transfer principles and generalizations thereof
- foundations of category theory
- extensions of set theory
- models of type theories
- algebraic approaches to programming and program derivation
- functional programming (esp. Haskell) and believing in high-level optimizations

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*.

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

- I have implemented an interpreter for algorithmic rule systems, which has proven to be a nice tool for imposing additional intensional structure on object logics in Isabelle. In particular this makes it possible to define custom type theories, where the type system has become an animation strategy of theorems about a semantic interpretation of types as Isabelle terms.
- The most concrete goal towards type-theoretic structure over set theory is to find a good intensional representation of an extension of Isabelle/ZF with a universe hierarchy, together with (local) inference of its verbosities. In the longer term I want to explore customizable proof terms, proof automation (classical, higher-order, bidirectional) with support for algorithmic rules systems and the architecture of the landscape of packages that are necessary for working comfortable in this vision of set theory.
- In my master's thesis I have designed an algorithmic rule system for the transfer of theory content under setoid isomorphisms.
- Integrated with algorithmic rule systems is an infrastructure for the propagation of facts under ''forward rules''. Forward rules that call out to the algorithmic rule system realizing isomorphic transfer make it possible to animate metatheories into usable packages. Only the input processing takes place with ML code in this approach, so it has a good chance to democratize package construction.
- The package for nonfree datatypes in Isabelle/HOL was realized as the animation of its formalized meta-theory using this general infrastructure. Inexpressivity and non-uniformities of HOL still make this a laborious task, but it does not require Isabelle/ML mastery. I am hopeful that a more expressive logic will allow a much more compact treatment of such an animation. To achieve a traditional user interface the processing of user input is still implemented in Isabelle/ML and delegates the actual constructions to the animation infrastructure. The main hurdles on the way towards a completely ML-free realization are a mechanism to bridge the gap between parsing and initial fact pools, nice error messages and HOL's lack of type constructor polymorphism, which makes it impossibe to state properties about a yet to be defined type constructor.
- Combining the Isabelle/HOL to Isabelle/ZF translation with a tool for transfer under isomorphisms in ZF, could walk us a long way towards a comfortable standard library in ZF. Reflecting some of HOL's intensional structure (esp. common usage forms of type classes) into ZF seems possible given the versatility of algorithmic rule systems.