BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Czech Republic
1 × Denmark
1 × Finland
1 × Germany
1 × Italy
1 × United Kingdom
2 × Estonia
2 × France
2 × Japan
2 × Poland
2 × Spain
3 × The Netherlands
4 × USA
Collaborated with:
P.Johann ∅ M.Abbott R.Atkey T.Altenkirch C.Lüth C.McBride V.d.Paiva E.Ritter A.Heyworth R.D.Cosmo F.N.Forsberg L.Malatesta C.Fumex R.Prince A.Setzer B.Jacobs T.Uustalu V.Vene T.Revell S.Staton P.Hancock
Talks about:
type (7) induct (5) contain (3) model (3) use (3) substitut (2) coproduct (2) construct (2) properti (2) explicit (2)

Person: Neil Ghani

DBLP DBLP: Ghani:Neil

Contributed to:

TLCA 20152015
POPL 20142014
LICS 20132013
TLCA 20132013
FOSSACS 20122012
FOSSACS 20112011
CSL 20102010
FLOPS 20082008
POPL 20082008
TLCA 20072007
ICFP 20052005
RTA 20052005
ICALP 20042004
FoSSaCS 20032003
RTA 20032003
TLCA 20032003
ICFP 20022002
FoSSaCS 19991999
ICALP 19981998
ICALP 19971997
TLCA 19971997
CSL 19961996
TLCA 19951995

Wrote 23 papers:

TLCA-2015-AtkeyGFRS #modelling #morphism #physics #polymorphism
Models for Polymorphism over Physical Dimension (RA, NG, FNF, TR, SS), pp. 45–59.
POPL-2014-AtkeyGJ #dependent type #parametricity #type system
A relationally parametric model of dependent type theory (RA, NG, PJ), pp. 503–516.
LICS-2013-GhaniMFS #data type
Fibred Data Types (NG, LM, FNF, AS), pp. 243–252.
TLCA-2013-HancockMGMA #induction #recursion
Small Induction Recursion (PH, CM, NG, LM, TA), pp. 156–172.
FoSSaCS-2012-AtkeyGJJ #induction
Fibrational Induction Meets Effects (RA, NG, BJ, PJ), pp. 42–57.
FoSSaCS-2011-AtkeyJG #induction #question #refinement
When Is a Type Refinement an Inductive Type? (RA, PJ, NG), pp. 72–87.
CSL-2010-GhaniJF #algebra #induction
Fibrational Induction Rules for Initial Algebras (NG, PJ, CF), pp. 336–350.
FLOPS-2008-PrinceGM #proving #using
Proving Properties about Lists Using Containers (RP, NG, CM), pp. 97–112.
POPL-2008-JohannG #data type #programming
Foundations for structured programming with GADTs (PJ, NG), pp. 297–308.
TLCA-2007-JohannG #algebra #exclamation #semantics
Initial Algebra Semantics Is Enough! (PJ, NG), pp. 207–222.
ICFP-2005-GhaniJUV #monad
Monadic augment and generalised short cut fusion (NG, PJ, TU, VV), pp. 294–305.
RTA-2005-AbbottGL #composition
Abstract Modularity (MA, NG, CL), pp. 46–60.
ICALP-2004-AbbottAG #induction #representation #using
Representing Nested Inductive Types Using W-Types (MA, TA, NG), pp. 59–71.
FoSSaCS-2003-AbbottAG #category theory
Categories of Containers (MA, TA, NG), pp. 23–38.
RTA-2003-GhaniH
A Rewriting Alternative to Reidemeister-Schreier (NG, AH), pp. 452–466.
TLCA-2003-AbbottAGM
Derivatives of Containers (MA, TA, NG, CM), pp. 16–30.
ICFP-2002-LuthG #monad #using
Composing monads using coproducts (CL, NG), pp. 133–144.
FoSSaCS-1999-GhaniPR #category theory #modelling
Categorical Models of Explicit Substitutions (NG, VdP, ER), pp. 197–211.
ICALP-1998-GhaniPR
Explicit Substitutions for Constructive Necessity (NG, VdP, ER), pp. 743–754.
ICALP-1997-CosmoG #composition #higher-order #on the #λ-calculus
On Modular Properties of Higher Order Extensional λ Calculi (RDC, NG), pp. 237–247.
TLCA-1997-Ghani #calculus #dependent type #type system
Eta-Expansions in Dependent Type Theory — The Calculus of Constructions (NG), pp. 164–180.
CSL-1996-Ghani
η-Expansions in Fω (NG), pp. 182–197.
TLCA-1995-Ghani
ßn-Equality for Coproducts (NG), pp. 171–185.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.