Zobrazeno 1 - 10
of 80
pro vyhledávání: '"Kaposi, Ambrus"'
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it
Externí odkaz:
http://arxiv.org/abs/2307.06448
Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed
Externí odkaz:
http://arxiv.org/abs/2302.05190
We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over the codomain of F. We rely on the
Externí odkaz:
http://arxiv.org/abs/2102.11649
Autor:
Kovács, András, Kaposi, Ambrus
Publikováno v:
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2020, Pages 648-661
Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic descriptions of type theori
Externí odkaz:
http://arxiv.org/abs/2006.11736
There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to refer to the syntax, for example in proofs of canonicity and normalisat
Externí odkaz:
http://arxiv.org/abs/1907.07562
Autor:
Kaposi, Ambrus, Kovács, András
Publikováno v:
Logical Methods in Computer Science, Volume 16, Issue 1 (February 13, 2020) lmcs:5173
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support e
Externí odkaz:
http://arxiv.org/abs/1902.00297
Autor:
Kaposi, Ambrus
Type theory (with dependent types) was introduced by Per Martin-Löf with the intention of providing a foundation for constructive mathematics. A part of constructive mathematics is type theory itself, hence we should be able to say what type theory
Externí odkaz:
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.713896
Autor:
Simon, Barbara, Ceglédi, Andrea, Dolgos, János, Farkas, Péter, Gaddh, Manila, Hankó, László, Horváth, Robert, Kaposi, Ambrus, Magyar, Lászlóné, Masszi, Tamás, Szederjesi, Attila, Wohner, Nikolett, Bodó, Imre ∗
Publikováno v:
In Blood 3 November 2022 140(18):1983-1992
Autor:
Altenkirch, Thorsten, Kaposi, Ambrus
Publikováno v:
Logical Methods in Computer Science, Volume 13, Issue 4 (October 23, 2017) lmcs:2588
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms o
Externí odkaz:
http://arxiv.org/abs/1612.02462
Autor:
Capriotti, Paolo, Kaposi, Ambrus
Publikováno v:
EPTCS 153, 2014, pp. 2-30
Applicative functors are a generalisation of monads. Both allow the expression of effectful computations into an otherwise pure language, like Haskell. Applicative functors are to be preferred to monads when the structure of a computation is fixed a
Externí odkaz:
http://arxiv.org/abs/1403.0749