Zobrazeno 1 - 10
of 82
pro vyhledávání: '"Brigitte Pientka"'
Publikováno v:
Journal of Formalized Reasoning, Vol 8, Iss 1, Pp 49-91 (2015)
When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effo
Externí odkaz:
https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 185, Iss Proc. LFMTP 2015, Pp 18-32 (2015)
A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with b
Externí odkaz:
https://doaj.org/article/d8c7ace32e1f4e2496dc81c64cd08fe0
Autor:
Andrew Cave, Brigitte Pientka
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 185, Iss Proc. LFMTP 2015, Pp 33-45 (2015)
Proofs by logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe the completeness proof of algorithmic equality for simply typ
Externí odkaz:
https://doaj.org/article/a3349533a8984de8b01a2d13bd51a81a
Autor:
Mathieu Boespflug, Brigitte Pientka
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 71, Iss Proc. LFMTP 2011, Pp 29-43 (2011)
Contextual type theory distinguishes between bound variables and meta-variables to write potentially incomplete terms in the presence of binders. It has found good use as a framework for concise explanations of higher-order unification, characterize
Externí odkaz:
https://doaj.org/article/4e563c3654cf4cd0b2a71e3472a01474
Autor:
Andreas Abel, Brigitte Pientka
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 34, Iss Proc. LFMTP 2010, Pp 5-20 (2010)
In this paper, we present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. We first present a dependently typed lambda calcu
Externí odkaz:
https://doaj.org/article/ae06bcb414f144f192e6b7717c5e3248
Autor:
Brigitte Pientka, Cesare Tinelli
This open access book constitutes the proceedings of the 29th International Conference on Automated Deduction, CADE 29, which took place in Rome, Italy, during July 2023. The 28 full papers and 5 short papers presented were carefully reviewed and se
Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:1-27
We describe the foundation of the metaprogramming language, Mœbius, which supports the generation of polymorphic code and, more importantly, the analysis of polymorphic code via pattern matching. Mœbius has two main ingredients: 1) we exploit conte
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d0c10ea475301ac44b06691e6ea3ce10
https://doi.org/10.1145/3498700
https://doi.org/10.1145/3498700
We describe the categorical semantics for a simply typed variant and a simplified dependently typed variant of Cocon , a contextual modal type theory where the box modality mediates between the weak function space that is used to represent higher-ord
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6174a5aa65d3b1f67b668518b0891f51
http://arxiv.org/abs/2206.02831
http://arxiv.org/abs/2206.02831
Publikováno v:
Programming Languages and Systems ISBN: 9783031210365
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::58ef3ac09e028ae64b05c54c133474b2
https://doi.org/10.1007/978-3-031-21037-2_10
https://doi.org/10.1007/978-3-031-21037-2_10
Autor:
Brigitte Pientka, Aliya Hameer
Publikováno v:
Proceedings of the ACM on Programming Languages. 3:1-15
Online programming platforms have immense potential to improve students' educational experience. They make programming more accessible, as no installation is required; and automatic grading facilities provide students with immediate feedback on their
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f11c4b62797f15483c9fb33121c3b8b4
https://doi.org/10.1145/3341719
https://doi.org/10.1145/3341719