Zobrazeno 1 - 10
of 131
pro vyhledávání: '"Felty, Amy"'
Autor:
de Maria, Elisabetta, Despeyroux, Joelle, Felty, Amy, Liò, Pietro, Olarte, Carlos, Bahrami, Abdorrahim
We advocate here the use of computational logic for systems biology, as a \emph{unified and safe} framework well suited for both modeling the dynamic behaviour of biological systems, expressing properties of them, and verifying these properties. The
Externí odkaz:
http://arxiv.org/abs/2007.07571
Autor:
Mahmoud, Mohamed Yousri, Felty, Amy P.
We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of Qu
Externí odkaz:
http://arxiv.org/abs/1812.03624
Publikováno v:
EPTCS 185, 2015, pp. 18-32
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:
http://arxiv.org/abs/1507.08052
A variety of logical frameworks support the use of higher-order abstract syntax (HOAS) in representing formal systems. Although these systems seem superficially the same, they differ in a variety of ways; for example, how they handle a context of ass
Externí odkaz:
http://arxiv.org/abs/1503.06095
We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological systems a
Externí odkaz:
http://arxiv.org/abs/1404.5439
Autor:
Martin, Alan J., Felty, Amy P.
Publikováno v:
EPTCS 71, 2011, pp. 76-90
Hybrid is a formal theory implemented in Isabelle/HOL that provides an interface for representing and reasoning about object languages using higher-order abstract syntax (HOAS). This interface is built around an HOAS variable-binding operator that is
Externí odkaz:
http://arxiv.org/abs/1111.0090
Autor:
Felty, Amy, Momigliano, Alberto
Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these difficulties
Externí odkaz:
http://arxiv.org/abs/0811.4367
Publikováno v:
In Electronic Notes in Theoretical Computer Science 26 October 2018 338:203-218
Autor:
Mahmoud, Mohamed Yousri, Felty, Amy P.
Publikováno v:
In Electronic Notes in Theoretical Computer Science 26 October 2018 338:185-201