Výsledky vyhledávání - "Arjen Rouvoet"

Intrinsically typed compilation with nameless labels

Autor: Arjen Rouvoet, Eelco Visser, Robbert Krebbers

Publikováno v: Proceedings of the ACM on Programming Languages, 5, 1-28
Proceedings of the ACM on Programming Languages, 5(POPL)
Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28

To avoid compilation errors it is desirable to verify that a compiler is type correct —i.e., given well-typed source code, it always outputs well-typed target code. This can be done intrinsically by implementing it as a function in a dependently ty

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::99a73c7b5a06b9b2e448aeca3b4bbdf0
https://doi.org/10.1145/3434303

Zobrazit plný text záznamu

Intrinsically-typed definitional interpreters à la carte

Autor: Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, Peter Mosses

Publikováno v: Proceedings of the ACM on Programming Languages, 6(OOPSLA2)

Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mec

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::063349af40b918e2849b82f9ccbe3bac
http://resolver.tudelft.nl/uuid:bfb4aaec-3a78-4a58-a788-cfd7e23991ba

Zobrazit plný text záznamu

Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications

Autor: Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Eelco Visser, Robbert Krebbers

Publikováno v: Proceedings of the ACM on Programming Languages, 4, 1-28
Proceedings of the ACM on Programming Languages, 4(OOPSLA)
Proceedings of the ACM on Programming Languages, 4, OOPSLA, pp. 1-28

There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automati

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c78da2333093d35e4690d0bf5d305431
http://hdl.handle.net/2066/228333

Zobrazit plný text záznamu

Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages

Autor: Eelco Visser, Casper Bach Poulsen, Arjen Rouvoet, Robbert Krebbers

Publikováno v: CPP

An intrinsically-typed definitional interpreter is a concise specification of dynamic semantics, that is executable and type safe by construction. Unfortunately, scaling intrinsically-typed definitional interpreters to more complicated object languag

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ee97b6c0b968560057f12ea7dce29103
http://resolver.tudelft.nl/uuid:913a5c7f-d521-445e-82af-a7771849f964

Zobrazit plný text záznamu

Intrinsically-Typed Definitional Interpreters for Imperative Languages

Autor: Arjen Rouvoet, Casper Bach Poulsen, Eelco Visser, Andrew Tolmach, Robbert Krebbers

Publikováno v: Proceedings of the ACM on Programming Languages, 2(POPL)

A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a se

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c449986e0011e9d40024c106b015bd66
http://resolver.tudelft.nl/uuid:4dc286fd-af6c-4d6b-a59b-bdf446550aa3

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání