Travelled to:1 × Brazil
1 × Cyprus
1 × Germany
2 × Portugal
2 × Spain
2 × The Netherlands
3 × Austria
3 × Poland
5 × France
5 × Italy
9 × USA
Collaborated with:B.C.Pierce S.Jost U.Schöpp T.Streicher N.Benton J.Hoffmann ∅ D.Wägner D.Rodriguez A.Karbyshev V.Nigam K.Aehlig H.Seidl T.Altenkirch G.Moser W.Chen E.Kitzelmann P.Baillot A.Kennedy L.Beringer U.D.Lago D.Aspinall D.Sannella K.Hammond H.Loidl A.Bauer R.Ramyaa U.Schreiweis H.Langendörfer P.Dybjer P.J.Scott N.Scaife
Talks about:program (8) analysi (8) resourc (6) type (6) amortis (5) order (5) logic (5) system (4) space (4) relat (4)
Person: Martin Hofmann
DBLP: Hofmann:Martin
Facilitated 1 volumes:
EdContributed to:
2015
2015
20142014
2013
2013
20132013
20122012201120112010
2010
201020102010
2010
2009
20092009200920092008200720062003200220011997199619951994
1990
1996Wrote 37 papers:
- PPDP-2015-Hofmann #analysis #automation
- Automatic amortized analysis (MH), p. 5.
- TLCA-2015-HofmannM #analysis #multi #term rewriting
- Multivariate Amortised Resource Analysis for Term Rewrite Systems (MH, GM), pp. 241–256.
- LICS-CSL-2014-0001C #abstract interpretation #automaton
- Abstract interpretation from Büchi automata (MH, WC), p. 10.
- POPL-2014-Benton0N #logic
- Abstract effects and proof-relevant logical relations (NB, MH, VN), pp. 619–632.
- BX-2013-HofmannPW
- Edit languages for information trees (MH, BCP, DW), pp. 76–89.
- ESOP-2013-HofmannR #analysis #automation #type inference
- Automatic Type Inference for Amortised Heap-Space Analysis (MH, DR), pp. 593–613.
- FoSSaCS-2013-BauerHK #higher-order #monad #on the #parametricity
- On Monadic Parametricity of Second-Order Functionals (AB, MH, AK), pp. 225–240.
- FoSSaCS-2013-HofmannRS #morphism #pointer #source code
- Pure Pointer Programs and Tree Isomorphism (MH, RR, US), pp. 321–336.
- TLCA-2013-BentonHN #generative #logic
- Proof-Relevant Logical Relations for Name Generation (NB, MH, VN), pp. 48–60.
- CAV-2012-0002AH #ml
- Resource Aware ML (JH, KA, MH), pp. 781–786.
- POPL-2012-HofmannPW #lens
- Edit lenses (MH, BCP, DW), pp. 495–508.
- BX-2011-Hofmann #lens #symmetry
- Symmetric lenses (MH), p. 60.
- POPL-2011-HoffmannAH #analysis #multi
- Multivariate amortized resource analysis (JH, KA, MH), pp. 357–370.
- POPL-2011-HofmannPW #lens #symmetry
- Symmetric lenses (MH, BCP, DW), pp. 371–384.
- ESOP-2010-HoffmannH #analysis #polynomial
- Amortized Resource Analysis with Polynomial Potential (JH, MH), pp. 287–306.
- ICALP-v2-2010-HofmannKS #functional #question #what
- What Is a Pure Functional? (MH, AK, HS), pp. 199–210.
- PEPM-2010-HofmannK #detection #morphism #problem #towards #using
- I/O guided detection of list catamorphisms: towards problem specific use of program templates in IP (MH, EK), pp. 93–100.
- POPL-2010-JostHLH #higher-order #resource management #source code
- Static determination of quantitative resource usage for higher-order programs (SJ, KH, HWL, MH), pp. 223–236.
- PPDP-2010-BaillotH #linear #logic #type inference
- Type inference in intuitionistic linear logic (PB, MH), pp. 219–230.
- SAS-2010-HofmannKS #coq #verification
- Verifying a Local Generic Solver in Coq (MH, AK, HS), pp. 340–355.
- CSL-2009-HofmannR #analysis #performance
- Efficient Type-Checking for Amortised Heap-Space Analysis (MH, DR), pp. 317–331.
- FM-2009-JostLHSH #analysis #bound #using
- “Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis (SJ, HWL, KH, NS, MH), pp. 354–369.
- LICS-2009-HofmannS #pointer #reachability #source code
- Pointer Programs and Undirected Reachability (MH, US), pp. 133–142.
- PPDP-2009-BentonKBH #higher-order #program transformation #relational #semantics
- Relational semantics for effect-based program transformations: higher-order store (NB, AK, LB, MH), pp. 301–312.
- TLCA-2009-LagoH #bound #linear #logic #revisited
- Bounded Linear Logic, Revisited (UDL, MH), pp. 80–94.
- CSL-2008-HofmannS #pointer #source code
- Pure Pointer Programs with Iteration (MH, US), pp. 79–93.
- PPDP-2007-BentonKBH #program transformation #relational #semantics
- Relational semantics for effect-based program transformations with dynamic allocation (NB, AK, LB, MH), pp. 87–96.
- ESOP-2006-HofmannJ #analysis #type system
- Type-Based Amortised Heap-Space Analysis (MH, SJ), pp. 22–37.
- POPL-2003-HofmannJ #first-order #functional #predict #source code
- Static prediction of heap space usage for first-order functional programs (MH, SJ), pp. 185–197.
- ESOP-2002-AspinallH #type system
- Another Type System for In-Place Update (DA, MH), pp. 36–52.
- LICS-2001-AltenkirchDHS #evaluation #normalisation #λ-calculus
- Normalization by Evaluation for Typed λ Calculus with Coproducts (TA, PD, MH, PJS), pp. 303–310.
- LICS-1997-HofmannS #continuation #modelling #λ-calculus #μ-calculus
- Continuation Models are Universal for λμ-Calculus (MH, TS), pp. 387–395.
- LICS-1996-AltenkirchHS #normalisation #polymorphism
- Reduction-Free Normalisation for a Polymorphic System (TA, MH, TS), pp. 98–106.
- POPL-1995-HofmannP #type system
- Positive Subtyping (MH, BCP), pp. 186–197.
- LICS-1994-HofmannS #proving
- The Groupoid Model Refutes Uniqueness of Identity Proofs (MH, TS), pp. 208–212.
- ECHT-1990-HofmannSL #approach #hypermedia #information management
- An Integrated Approach of Knowledge Acquisition by the Hypertext System CONCORDE (MH, US, HL), pp. 166–179.
- TAPSOFT-J-1995-HofmannS96 #abstraction #behaviour #higher-order #logic #on the
- On Behavioural Abstraction and Behavioural Satisfaction in Higher-Order Logic (MH, DS), pp. 3–45.