If you made any changes in Pure these will be visible here soon.

Research Output 2008 2020

8 Citations (Scopus)

When is a type refinement an inductive type

Atkey, R., Johann, P. & Ghani, N., 2011, Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011. Hofmann, M. (ed.). Springer, p. 72-87 16 p. (Lecture Notes in Computer Science ; vol. 6604).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Computer programming languages
22 Downloads (Pure)

Variations on inductive-recursive definitions

Ghani, N., McBride, C., Nordvall Forsberg, F. & Spahn, S., 30 Nov 2017, Proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science. Germany, 13 p. 63. (Leibniz International Proceedings in Informatics ).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Algebra
Chemical analysis
4 Downloads (Pure)

Universal properties for universal types in bifibrational parametricity

Ghani, N., Nordvall Forsberg, F. & Orsanigo, F., 30 Jun 2019, In : Mathematical Structures in Computer Science. 29, 6, p. 810–827 18 p.

Research output: Contribution to journalArticle

Open Access
File
Uniformity
Lemma
Semantics
Theorem
Model
1 Downloads (Pure)

Three equivalent ordinal notation systems in cubical Agda

Nordvall Forsberg, F., Xu, C. & Ghani, N., 24 Jan 2020, CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, p. 172–185 14 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Innovation
9 Citations (Scopus)

Small induction recursion

Hancock, P., McBride, C., Ghani, N., Malatesta, L. & Altenkirch, T., 6 Jun 2013, Typed Lambda Calculus and Applications: 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. Hasegawa, M. (ed.). Berlin: Springer, p. 156-172 17 p. (Lecture Notes in Computer Science; vol. 7941).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Containers
Polynomials
26 Downloads (Pure)

Representations of stream processors using nested fixed points

Hancock, P., Pattinson, D. & Ghani, N., 15 Sep 2009, In : Logical Methods in Computer Science. 5, 3, p. 1-17 17 p., 9.

Research output: Contribution to journalArticle

Open Access
File
Fixed point
Continuous Function
Fixpoint
Justification
Elimination
10 Citations (Scopus)
58 Downloads (Pure)

Refining inductive types

Atkey, R., Johann, P. & Ghani, N., 4 Jun 2012, In : Logical Methods in Computer Science. 8, 2, 30 p., 9.

Research output: Contribution to journalArticle

File
Refining
Refinement
Computer programming languages
Programming
Type Systems
2 Citations (Scopus)
12 Downloads (Pure)

Proof-relevant parametricity

Ghani, N., Nordvall Forsberg, F. & Orsanigo, F., 25 Mar 2016, A List of Successes That Can Change the World. Lindley, S., McBride, C., Trinder, P. & Sannella, D. (eds.). Switzerland: Springer-Verlag, p. 109-131 23 p. (Lecture Notes in Computer Science; vol. 9600).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Computer programming languages
Type Theory
Programming Languages
High-dimensional
Express

Positive inductive-recursive definitions

Ghani, N., Malatesta, L. & Nordvall Forsberg, F., 8 Aug 2013, Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013. Proceedings. Heckel, R. & Milius, S. (eds.). Berlin, p. 19-33 15 p. (Lecture Notes in Computer Science; vol. 8089).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Algebra
57 Downloads (Pure)

Positive inductive-recursive definitions

Ghani, N., Nordvall Forsberg, F. & Malatesta, L., 27 Mar 2015, In : Logical Methods in Computer Science. 11, 1, 13.

Research output: Contribution to journalArticle

Open Access
File
Recursive functions
Algebra
Functor
Morphisms
Recursive Functions
4 Citations (Scopus)
132 Downloads (Pure)

Parametric polymorphism - universally

Ghani, N., Nordvall Forsberg, F. & Orsanigo, F., 24 Jun 2015, Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. de Paiva, V., de Queiroz, R., Moss, L. S., Leivant, D. & de Oliveira, A. G. (eds.). p. 81-92 12 p. (Lecture Notes in Computer Science; vol. 9160).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Polymorphism
Semantics
13 Citations (Scopus)

Modularity and implementation of mathematical operational semantics

Jaskelioff, M., Ghani, N. & Hutton, G., 8 Mar 2011, In : Electronic Notes in Theoretical Computer Science. 229, 5, p. 75-95 21 p.

Research output: Contribution to journalArticle

Operational Semantics
Modularity
Semantics
Categorical
Structural Operational Semantics
64 Downloads (Pure)

Models for polymorphism over physical dimensions

Atkey, R., Ghani, N., Nordvall Forsberg, F., Revell, T. & Staton, S., 2015, 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15). Altenkirch, T. (ed.). Wadern, Germany , p. 999-1013 15 p. (Leibniz International Proceedings in Informatics (LIPIcs)).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Type Theory
Polymorphism
Relational Model
Fibration
Group Action
10 Citations (Scopus)
126 Downloads (Pure)

Indexed induction and coinduction, fibrationally.

Ghani, N., Johann, P. & Fumex, C., 2011, Algebra and coalgebra in computer science : Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Corradini, A., Klin, B. & Cirstea, C. (eds.). Springer, p. 176-191 15 p. (Lecture Notes in Computer Science; vol. 6859 ).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

File
Coinduction
Proof by induction
Fibration
Equality
Quotient
7 Citations (Scopus)

Generic fibrational induction

Ghani, N., Johann, P. & Fumex, C., 19 Jun 2012, In : Logical Methods in Computer Science. 8, 2, 12.

Research output: Contribution to journalArticle

Rule Induction
Proof by induction
Polynomials
Hyperfunctions
Syntactics
18 Citations (Scopus)
228 Downloads (Pure)

Foundations for structured programming with GADTs

Johann, P. & Ghani, N., 2008, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008. p. 297-308 12 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

File
Structured programming
Algebra
Semantics
Functional programming
Syntactics
2 Citations (Scopus)

Fibred data types

Ghani, N., Malatesta, L., Nordvall Forsberg, F. & Setzer, A., 2013, 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS). New York: IEEE, p. 243-252 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Semantics
Set theory
Computer programming languages
Data structures
12 Citations (Scopus)
57 Downloads (Pure)

Fibrational induction rules for initial algebras

Ghani, N., Johann, P. & Fumex, C., 2010, Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Dawar, A. & Veith, H. (eds.). Springer, Vol. 6247. p. 336-350 15 p. (Lecture Notes In Computer Science; vol. 6247).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

File
Algebra
Polynomials
Syntactics
Data structures
Semantics
10 Citations (Scopus)
41 Downloads (Pure)

Fibrational induction meets effects

Atkey, R., Ghani, N., Jacobs, B. & Johann, P., 2012, Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2011. Birkedal, L. (ed.). Springer, Vol. 7213. p. 42-57 16 p. (Lecture Notes in Computer Science; vol. 7213).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Syntactics
Semantics
Polynomials
1 Citation (Scopus)

Containers, monads and induction recursion

Ghani, N. & Hancock, P., 1 Jan 2016, In : Mathematical Structures in Computer Science. 26, Special Issue 01, p. 89-113 25 p.

Research output: Contribution to journalSpecial issue

Monads
Container
Recursion
Containers
Proof by induction
1 Citation (Scopus)
180 Downloads (Pure)

Comprehensive parametric polymorphism: categorical models and type theory

Ghani, N., Nordvall Forsberg, F. & Simpson, A., 22 Mar 2016, Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Jacobs, B. & Löding, C. (eds.). Vol. 9634. p. 3-19 17 p. (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Polymorphism
5 Downloads (Pure)
Open Access
File
Game theory
Probability distributions
7 Citations (Scopus)
53 Downloads (Pure)

Compositional game theory

Ghani, N., Hedges, J., Winschel, V. & Zahn, P., 12 Jul 2018, Proceedings of the Symposium on Logic in Computer Science (LICS) 2018. New York, 10 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Game theory
Economics
Computer science
Byproducts
Visualization
2 Citations (Scopus)
96 Downloads (Pure)

Bifibrational functorial semantics of parametric polymorphism

Ghani, N., Johann, P., Forsberg, F. N., Orsanigo, F. & Revell, T., 21 Dec 2015, In : Electronic Notes in Theoretical Computer Science. 319, p. 165-181 17 p.

Research output: Contribution to journalArticle

Open Access
File
Polymorphism
Semantics
Categorical
Invariance
Algebra
10 Citations (Scopus)
1 Downloads (Pure)

A universe of strictly positive families

Morris, P., Altenkirch, T. & Ghani, N., Feb 2009, In : International Journal of Foundations of Computer Science. 20, 1, p. 83-107 25 p.

Research output: Contribution to journalArticle

12 Citations (Scopus)
8 Downloads (Pure)

A relationally parametric model of dependent type theory

Atkey, R., Ghani, N. & Johann, P., 24 Jan 2014, POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT: Symposium on Principles of Programming Languages. New York, NY., p. 503-515 13 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Open Access
File
Algebra
Invariance
2 Citations (Scopus)
66 Downloads (Pure)

A principled approach to programming with nested types in Haskell

Johann, P. & Ghani, N., 30 Jun 2009, In : Higher-Order and Symbolic Computation. 22, 2, p. 155-189 35 p.

Research output: Contribution to journalArticle

Computer programming
Algebra
Semantics
Functional programming
Religious buildings
2 Citations (Scopus)
24 Downloads (Pure)

A compositional treatment of iterated open games

Ghani, N., Kupke, C., Lambert, A. & Nordvall Forsberg, F., 12 Sep 2018, In : Theoretical Computer Science. 741, p. 48-57 10 p.

Research output: Contribution to journalArticle

Open Access
File
Game
Economics
Game theory
Infinite Games
Compositionality