Zobrazeno 1 - 10
of 114
pro vyhledávání: '"McBride, Conor"'
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of $\alpha$-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on.
Externí odkaz:
http://arxiv.org/abs/2001.11001
Autor:
McBride, Conor
Publikováno v:
EPTCS 275, 2018, pp. 53-69
The key to any nameless representation of syntax is how it indicates the variables we choose to use and thus, implicitly, those we discard. Standard de Bruijn representations delay discarding maximally till the leaves of terms where one is chosen fro
Externí odkaz:
http://arxiv.org/abs/1807.04085
We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar's effect handler abstraction. Effect handler
Externí odkaz:
http://arxiv.org/abs/1611.09259
Autor:
McBride, Conor
Research in dependent type theories [ML71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of the computational aspects of type theory for programmi
Externí odkaz:
http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561753
The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, frustrating users with type errors arising when evaluation fails to iden
Externí odkaz:
http://arxiv.org/abs/1304.0809
Ornaments aim at taming the multiplication of special-purpose datatype in dependently-typed theory. In its original form, the definition of ornaments is tied to a particular universe of datatypes. Being a type theoretic object, constructions on ornam
Externí odkaz:
http://arxiv.org/abs/1212.3806
We present an elaboration of inductive definitions down to a universe of datatypes. The universe of datatypes is an internal presentation of strictly positive families within type theory. By elaborating an inductive definition -- a syntactic artifact
Externí odkaz:
http://arxiv.org/abs/1210.6390
Publikováno v:
Advanced Mathematical and Computational Tools in Metrology and Testing XII
Type systems can be used for tracking dimensional consistency of numerical computations: we present an extension from dimensions of scalar quantities to dimensions of vectors and matrices, making use of dependent types from programming language theor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::da91fa78dd03042b48a7342332ac4444
https://doi.org/10.1142/9789811242380_0020
https://doi.org/10.1142/9789811242380_0020
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
Journal of Reconstructive Microsurgery Open; January 2023, Vol. 8 Issue: 1 pe54-e59, 6p
