Zobrazeno 1 - 10
of 64
pro vyhledávání: '"Thorsten Altenkirch"'
Autor:
Thorsten Altenkirch, Ambrus Kaposi
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 4 (2017)
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:
https://doaj.org/article/5a2428747d114556b3bc2d24b9bdf32e
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 1 (2017)
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have uniqu
Externí odkaz:
https://doaj.org/article/2ab86f20a0484d0e8ba1fce1ce0ad8ad
Publikováno v:
Journal of Formalized Reasoning, Vol 7, Iss 1, Pp 1-43 (2014)
Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed
Externí odkaz:
https://doaj.org/article/5c63aaa6e856443f89239e99e5bb92ac
Autor:
Thorsten Altenkirch
Publikováno v:
Mathematical Structures in Computer Science. 31:953-957
My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type Theory while sharing some memories of Martin.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9eda393ab682f93d0444b7e766330cfc
https://doi.org/10.1017/s0960129520000316
https://doi.org/10.1017/s0960129520000316
Publikováno v:
Proceedings of the ACM on Programming Languages. 3:1-24
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1e3a4b3902f9304461971b6dea25acd9
https://doi.org/10.1145/3290315
https://doi.org/10.1145/3290315
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030719944
FoSSaCS
FoSSaCS
The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent pr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::daaca4f5664a1587ab4934392ea4d8b6
https://doi.org/10.1007/978-3-030-71995-1_1
https://doi.org/10.1007/978-3-030-71995-1_1
Autor:
Luis Scoccola, Thorsten Altenkirch
Publikováno v:
LICS
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c44e066d7ecc17880cb9aa62d148e50c
https://doi.org/10.1145/3373718.3394760
https://doi.org/10.1145/3373718.3394760
Publikováno v:
MPC 2019-13th International Conference on Mathematics of Program Construction
MPC 2019-13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩
Lecture Notes in Computer Science ISBN: 9783030336356
MPC
Mathematics of Program Construction-13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Mathematics of Program Construction
MPC 2019-13th International Conference on Mathematics of Program Construction, Oct 2019, Porto, Portugal. pp.155-196, ⟨10.1007/978-3-030-33636-3_7⟩
Lecture Notes in Computer Science ISBN: 9783030336356
MPC
Mathematics of Program Construction-13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Mathematics of Program Construction
International audience; We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying function extensionality, propositional extensionality and a definitional computation
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::38692a54b8393b5e043ccedfaabb70f2
https://hal.inria.fr/hal-02281225/document
https://hal.inria.fr/hal-02281225/document
Autor:
Ambrus Kaposi, Thorsten Altenkirch
Publikováno v:
POPL
We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::13075a8c4c2d981fbe85dc129dd24d61
https://doi.org/10.1145/2914770.2837638
https://doi.org/10.1145/2914770.2837638
Publikováno v:
IFL
Agent-Based Simulation (ABS) is a methodology in which a system is simulated in a bottom-up approach by modelling the micro interactions of its constituting parts, called agents, out of which the global system behaviour emerges.So far mainly object-o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5df4ebf326475fbeb82480b63b909387
https://doi.org/10.1145/3310232.3310372
https://doi.org/10.1145/3310232.3310372