`Travelled to:`

1 × Germany

1 × Poland

1 × Portugal

1 × Spain

1 × The Netherlands

1 × USA

1 × United Kingdom

2 × France

`Collaborated with:`

∅ R.Nederpelt G.I.Jojgov B.Werner J.Endrullis H.Zantema E.Poll J.Zwanenburg F.Barbanera M.Fernández D.Kühlwein J.Urban E.Tsivtsivadze T.Heskes

`Talks about:`

type (5) theori (3) second (3) properti (2) rosser (2) rewrit (2) depend (2) church (2) proof (2) order (2)

## Person: Herman Geuvers

### DBLP: Geuvers:Herman

### Contributed to:

### Wrote 10 papers:

- KDIR-2011-KuhlweinUTGH #automation #multi #ranking #reasoning
- Multi-output Ranking for Automated Reasoning (DK, JU, ET, HG, TH), pp. 42–51.
- CSL-2009-EndrullisGZ #term rewriting
- Degrees of Undecidability in Term Rewriting (JE, HG, HZ), pp. 255–270.
- RTA-2004-GeuversN #deduction
- Rewriting for Fitch Style Natural Deductions (HG, RN), pp. 134–154.
- CSL-2002-GeuversJ #interactive #logic #proving
- Open Proofs and Open Terms: A Basis for Interactive Logic (HG, GIJ), pp. 537–552.
- TLCA-2001-Geuvers #dependent type #higher-order #induction #type system
- Induction Is Not Derivable in Second Order Dependent Type Theory (HG), pp. 166–181.
- CSL-1999-GeuversPZ #proving #type system
- Safe Proof Checking in Type Theory with Y (HG, EP, JZ), pp. 439–452.
- CSL-1996-Geuvers #dependent type #higher-order #logic #modelling #type system
- Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory (HG), pp. 167–181.
- LICS-1994-BarbaneraFG #algebra #composition #confluence #normalisation
- Modularity of Strong Normalization and Confluence in the algebraic-λ-Cube (FB, MF, HG), pp. 406–415.
- LICS-1994-GeuversW #on the #type system
- On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study (HG, BW), pp. 320–329.
- LICS-1992-Geuvers #λ-calculus
- The Church-Rosser Property for βη-reduction in Typed λ-Calculi (HG), pp. 453–460.