Zobrazeno 1 - 10
of 16
pro vyhledávání: '"Nicolai Kraus"'
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
Autor:
Andreas Abel, Nicolai Kraus
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 71, Iss Proc. LFMTP 2011, Pp 1-13 (2011)
We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional information where
Externí odkaz:
https://doaj.org/article/34c72e77e3494eff8e2aa801bec6374d
Autor:
Nicolai Kraus, Jakob Von Raumer
Publikováno v:
Mathematical Structures in Computer Science, 32 (7), 982–1014
Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b25e56a5be0ae2965e4cf53fe7d5d4c8
https://doi.org/10.1017/s0960129523000026
https://doi.org/10.1017/s0960129523000026
Autor:
Nicolai Kraus
Publikováno v:
LICS
Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer'
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::59a21d4b95481fa1adc5e10f30ac08a5
https://doi.org/10.1109/lics52264.2021.9470667
https://doi.org/10.1109/lics52264.2021.9470667
Publikováno v:
MFCS 2021
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=r3c4b2081b22::1b49fe0e5c463f2074fa9f7f7646e95f
Publikováno v:
ICPS
In networked operating room environments, there is an emerging trend towards standardized non-proprietary communication protocols which allow to build new integration solutions and flexible human-machine interaction concepts. The most prominent endea
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::37e2a7c00bb264217b430c1002933d08
https://doi.org/10.1109/icps48405.2020.9274729
https://doi.org/10.1109/icps48405.2020.9274729
Autor:
Nicolai Kraus, Jakob von Raumer
Publikováno v:
LICS
Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of inducti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f53ad9df8de9bc23dc5ad1c7bb2c69f0
http://arxiv.org/abs/2001.07655
http://arxiv.org/abs/2001.07655
Autor:
Jakob von Raumer, Nicolai Kraus
Publikováno v:
LICS
The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pus
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bc6cf10d5ac91a07fa87889cde90bbb2
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030336356
MPC
MPC
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:
https://explore.openaire.eu/search/publication?articleId=doi_________::1a57016943a4ac8486785e882952fd5b
https://doi.org/10.1007/978-3-030-33636-3_12
https://doi.org/10.1007/978-3-030-33636-3_12
Autor:
Thorsten Altenkirch, Fredrik Nordvall Forsberg, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319893655
FoSSaCS
FoSSaCS
Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, su
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::228400bde5f2f34b2264640f02316869
https://strathprints.strath.ac.uk/63612/1/Altenkirch_etal_FSSCS_2018_Quotient_inductive_inductive.pdf
https://strathprints.strath.ac.uk/63612/1/Altenkirch_etal_FSSCS_2018_Quotient_inductive_inductive.pdf