Zobrazeno 1 - 10
of 82
pro vyhledávání: '"Nominal Logic"'
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.
Autor:
Fernández, Maribel
In this talk we discuss the nominal approach to the specification of languages with binders and some applications to programming languages and verification.
LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and
LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b9528b12f6c816eba13d78b90b61ae63
Autor:
Cheney, James, Fernández, Maribel
Publikováno v:
Cheney, J & Fernández, M 2022, Nominal Matching Logic . in Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022) ., 5, 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, 20/09/22 . https://doi.org/10.1145/3551357.3551375
We introduce Nominal Matching Logic (NML) as an extension of Matching Logic with names and binding following the Gabbay-Pitts nominal approach. Matching logic is the foundation of the $\mathbb{K}$ framework, used to specify programming languages and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::afe20f26ab7054466396c3279fb53ef0
http://arxiv.org/abs/2207.14139
http://arxiv.org/abs/2207.14139
Autor:
James Cheney, Alberto Momigliano
Publikováno v:
Cheney, J & Momigliano, A 2017, ' αCheck: a mechanized metatheory model-checker ', Theory and Practice of Logic Programming, vol. 17, no. 3, pp. 311-352 . https://doi.org/10.1017/S1471068417000035
The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::db834a2c263041418a2d2222c19f10a3
https://doi.org/10.1017/s1471068417000035
https://doi.org/10.1017/s1471068417000035
Publikováno v:
Repositório Institucional do IBICT
instacron:IBICT
Instituto Brasileiro de Informação Ciência e Tecnologia
Datacite
LAReferencia-Red Federada de Repositorios Institucionales de Publicaciones Científicas Latinoamericanas
Zenodo
ZENODO
instacron:IBICT
Instituto Brasileiro de Informação Ciência e Tecnologia
Datacite
LAReferencia-Red Federada de Repositorios Institucionales de Publicaciones Científicas Latinoamericanas
Zenodo
ZENODO
Submitted by Washington Segundo (washingtonsegundo@ibict.br) on 2019-05-06T16:02:20Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) thesis20190319.pdf: 2460573 bytes, checksum: a110e47747c4883105433dc23db4
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::502d19725b02566a73df49659cedda77
https://zenodo.org/record/2582109
https://zenodo.org/record/2582109
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.
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.
Autor:
Ayala-Rincón, Mauricio, de Carvalho-Segundo, Washington, Fernández, Maribel, Nantes-Sobrinho, Daniele
Publikováno v:
Ayala-Rincón, M, de Carvalho-Segundo, W, Fernández, M & Nantes-Sobrinho, D 2017, ' A Formalisation of Nominal α-equivalence with A and AC Function Symbols : LSFA 2016-11th Workshop on Logical and Semantic Frameworks with Applications (LSFA) ', Electronic Notes in Theoretical Computer Science, vol. 332, pp. 21-38 . https://doi.org/10.1016/j.entcs.2017.04.003
A formalisation of soundness of the notion of α-equivalence in nominal abstract syntax modulo associative (A) and associative-commutative (AC) equational theories is described. Initially, the notion of α-equivalence is specified based on a so calle
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od______2761::f170cb7e09e9785849867a04429c6d50
https://kclpure.kcl.ac.uk/ws/files/71666384/A_Formalisation_of_Nominal_AYALA_RINCON_Publishedonline22June2017_GOLD_VoR_CC_BY_NC_ND_.pdf
https://kclpure.kcl.ac.uk/ws/files/71666384/A_Formalisation_of_Nominal_AYALA_RINCON_Publishedonline22June2017_GOLD_VoR_CC_BY_NC_ND_.pdf
Autor:
Stefan Berghofer, Christian Urban
Publikováno v:
Electronic Notes in Theoretical Computer Science. 174(5):53-67
Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nominal approaches come close to the style of reasoning employed in informal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1f0ad8e4eae6ac1484b45e76f1d9971c
Autor:
Johannes Åman Pohjola, Joachim Parrow
Publikováno v:
CPP
Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0a3e3340df1c07d24b6dda46dbec4023
https://doi.org/10.1145/2854065.2854080
https://doi.org/10.1145/2854065.2854080