Zobrazeno 1 - 10
of 116
pro vyhledávání: '"Nadathur, Gopalan"'
Autor:
Gray, Terrance, Nadathur, Gopalan
Publikováno v:
EPTCS 404, 2024, pp. 19-34
When reasoning about formal objects whose structures involve binding, it is often necessary to analyze expressions relative to a context that associates types, values, and other related attributes with variables that appear free in the expressions. W
Externí odkaz:
http://arxiv.org/abs/2407.06625
This paper concerns the development of metatheory for extensible languages. It uses as its starting point a view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of
Externí odkaz:
http://arxiv.org/abs/2312.14374
Autor:
Holte, Steven, Nadathur, Gopalan
The ability to compose code in a modular fashion is important to the construction of large programs. In the logic programming setting, it is desirable that such capabilities be realized through logic-based devices. We describe an approach for doing t
Externí odkaz:
http://arxiv.org/abs/2303.10453
Autor:
Nadathur, Gopalan
The POPLMARK Challenge comprises a set of problems intended to measure the strength of reasoning systems in the realm of mechanizing programming language meta-theory at the time the challenge was enunciated. Included in the collection is the exercise
Externí odkaz:
http://arxiv.org/abs/2112.09274
Autor:
Nadathur, Gopalan, Southern, Mary
Felty and Miller have described what they claim to be a faithful encoding of the dependently typed lambda calculus LF in the logic of hereditary Harrop formulas, a sublogic of an intuitionistic variant of Church's Simple Theory of Types. Their encodi
Externí odkaz:
http://arxiv.org/abs/2108.10848
Autor:
Southern, Mary, Nadathur, Gopalan
Publikováno v:
EPTCS 337, 2021, pp. 104-120
We present a system called Adelfa that provides mechanized support for reasoning about specifications developed in the Edinburgh Logical Framework or LF. Underlying Adelfa is a new logic named L_LF. Typing judgements in LF are represented by atomic f
Externí odkaz:
http://arxiv.org/abs/2107.07666
Autor:
Nadathur, Gopalan, Southern, Mary
We present a logic named L_{LF} whose intended use is to formalize properties of specifications developed in the dependently typed lambda calculus LF. The logic is parameterized by the LF signature that constitutes the specification. Atomic formulas
Externí odkaz:
http://arxiv.org/abs/2107.00111
Autor:
Southern, Mary, Nadathur, Gopalan
We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF serve as atomic formulas, and quantification is permitted over contexts and terms that might appe
Externí odkaz:
http://arxiv.org/abs/1806.10199
Autor:
Nadathur, Gopalan, Wang, Yuting
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that ar
Externí odkaz:
http://arxiv.org/abs/1806.07523
Autor:
Wang, Yuting, Nadathur, Gopalan
We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. O
Externí odkaz:
http://arxiv.org/abs/1509.03705