Foundations for structured programming with GADTs P Johann, N Ghani Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2008 | 94 | 2008 |

A relationally parametric model of dependent type theory R Atkey, N Ghani, P Johann Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 78 | 2014 |

Free theorems in the presence of *seq*P Johann, J Voigtländer Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2004 | 69 | 2004 |

A generic operational metatheory for algebraic effects P Johann, A Simpson, J Voigtländer 2010 25th Annual IEEE Symposium on Logic in Computer Science, 209-218, 2010 | 62 | 2010 |

Initial algebra semantics is enough! P Johann, N Ghani Typed Lambda Calculi and Applications: 8th International Conference, TLCA …, 2007 | 54 | 2007 |

Deduction systems R Socher-Ambrosius, P Johann Springer Science & Business Media, 2012 | 49 | 2012 |

The impact of seq on free theorems-based program transformations P Johann, J Voigtländer Fundamenta Informaticae 69 (1-2), 63-102, 2006 | 47 | 2006 |

A generalization of short-cut fusion and its correctness proof P Johann Higher-order and symbolic computation 15, 273-300, 2002 | 45 | 2002 |

Warm fusion in Stratego: A case study in generation of program transformation systems P Johann, E Visser Annals of Mathematics and Artificial Intelligence 29, 1-34, 2000 | 41 | 2000 |

Indexed induction and coinduction, fibrationally N Ghani, P Johann, C Fumex arXiv preprint arXiv:1307.3263, 2013 | 40 | 2013 |

An improved general E-unification method DJ Dougherty, P Johann Journal of symbolic computation 14 (4), 303-320, 1992 | 39 | 1992 |

Fibrational induction rules for initial algebras N Ghani, P Johann, C Fumex Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual …, 2010 | 30 | 2010 |

Short cut fusion: Proved and improved P Johann Semantics, Applications, and Implementation of Program Generation: Second …, 2001 | 30 | 2001 |

Short cut fusion is correct P Johann Journal of Functional Programming 13 (4), 797-814, 2003 | 29 | 2003 |

Bifibrational functorial semantics of parametric polymorphism N Ghani, P Johann, FN Forsberg, F Orsanigo, T Revell Electronic Notes in Theoretical Computer Science 319, 165-181, 2015 | 27 | 2015 |

Generic fibrational induction N Ghani, P Johann, C Fumex arXiv preprint arXiv:1206.0357, 2012 | 27 | 2012 |

Short cut fusion of recursive programs with computational effects N Ghani, P Johann Symposium on Trends in Functional Programming (TFP 2008), 2008 | 24 | 2008 |

A combinatory logic approach to higher-order *E*-unificationDJ Dougherty, P Johann Automated Deduction—CADE-11: 11th International Conference on Automated …, 1992 | 24 | 1992 |

Staged notational definitions W Taha, P Johann Generative Programming and Component Engineering: Second International …, 2003 | 23 | 2003 |

Selective strictness and parametricity in structural operational semantics, inequationally J Voigtländer, P Johann Theoretical Computer Science 388 (1-3), 290-318, 2007 | 22 | 2007 |