Jan HoffmannI am a Postdoctoral Associate in the FLINT Group at the Department of Computer Science of Yale University. My research interests include verification of low-level code, type systems, quantitative resource analysis of programs, theorem proving, algorithmic game theory, and SAT solving. Prior to joining Yale, I was a PhD student inTheoretical Computer Science Group at LMU Munich and a scholar of the DFG Research Training Group PUMA. My advisor was Martin Hofmann. Before that, I studied computer science at the LMU as a scholar of the German National Academic Foundation. |
|
Coordinates
|
uni (at) hoffjan . de GnuPG Key |
|
| phone | +1 (203) 432 1267 |
| office | E105 |
| address | Department of Computer Science Yale University 51 Prospect Street 06511 New Haven, CT USA |
Projects
- Resource Aware ML: A functional programming language that automatically computes resource bounds at compile time.
Theses
-
Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis
Dissertation, Ludwig-Maximilians-Universität München
2011
pdf | BibTex | Printed copy at epubli -
Resolution Proofs and DLL-Algorithms with Clause Learning
Diploma Thesis, Ludwig-Maximilians-Universität München
2007
pdf (A4 paper) | pdf (letter paper) | BibTex
Journal Papers
-
The Computational Complexity of Weak Saddles
Theory of Computing Systems (to appear)
2010 (The conference version appeared at SAGT'09)
pdf | link -
Computing Shapley's Saddles
ACM SIGecom Exchanges, 8(2)
2009
pdf | link -
Finding a Tree Structure in a Resolution Proof is NP-complete
Theoretical Computer Science 410, 2295-2300
2009
pdf | BibTex | link -
Resolution Trees with Lemmas - Resolution Refinements that Characterize DLL-Algorithms with Clause Learning
Logical Methods in Computer Science Vol. 4 (4:13) 2008
2008
pdf | BibTex | link -
The NP-hardness of Finding a Directed Acyclic Graph for
Regular Resolution
Theoretical Computer Science 396, 271-276
2008
pdf | BibTex | link
Conference Papers
-
Higher-Order Functional Reactive Programming in Bounded Space
In Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12) (To appear)
2012
pdf -
Multivariate Amortized Resource Analysis
In Proceedings of the 38th Symposium on Principles of Programming Languages (POPL'11)
2011
pdf | BibTex | link -
Amortized Resource Analysis with Polymorphic Recursion
and Partial Big-Step Operational Semantics
In Proceedings of the 8th Asian Symposium on Programming Languages (APLAS'10)
2010
pdf (exteded version) | pdf (conference version) | BibTex | link -
Amortized Resource Analysis with Polynomial Potential - A
Static Inference of Polynomial Bounds for Functional Programs
In Proceedings of the 19th European Symposium on Programming (ESOP'10), Lecture Notes in Computer Science, volume 6012, pages 287-306
2010
pdf (extended version) | pdf (conference version) | BibTex | link -
The Complexity of Computing Minimal Unidirectional Covering Sets
In Proceedings of the 7th International Conference on Algorithms and Complexity (CIAC'10), Lecture Notes in Computer Science
2010
pdf | link -
The Computational Complexity of Weak Saddles
In Proceedings of the 2nd International Symposium on Algorithmic Game Theory (SAGT'09), Lecture Notes in Computer Science, volume 5814, pages 238–249
2009
pdf | BibTex | link
Drafts and Technical Reports
-
Multivariate Amortized Resource Analysis
Full version of the POPL'11 article. Submitted.
2011
pdf -
Analyzing Sorting Algorithms in Resource Aware ML
TUM Technical Report (to appear)
2011
pdf -
Weak Parity Games and Language Containment
of Weak Alternating Parity Automata
Project Work
2006
pdf
Recent Teaching
- WS 2008/09 Komplexitätstheorie (with Martin Hofmann)
- WS 2007/08 Repetitorium Informatik 1 (with Jan Johannsen)
Misc
- My Erdös number is 3 due to the path JH - Samuel R. Buss - Shlomo Moran - PE.