Zobrazeno 1 - 10
of 158
pro vyhledávání: '"68N15"'
Autor:
Warren, David S.
This paper describes a semantics for pure Prolog programs with negation that provides meaning to metaprograms. Metaprograms are programs that construct and use data structures as programs. In Prolog a primary mataprogramming construct is the use of a
Externí odkaz:
http://arxiv.org/abs/2408.07652
Autor:
Platzer, André
Publikováno v:
Formal Methods Teaching 2024
This invited paper is a passionate pitch for the significance of logic in scientific education. Logic helps focus on the essential core to identify the foundations of ideas and provides corresponding longevity with the resulting approach to new and o
Externí odkaz:
http://arxiv.org/abs/2407.09959
This paper unites two research lines. The first involves finding categorical models of quantum programming languages and their type systems. The second line concerns the program of quantization of mathematical structures, which amounts to finding non
Externí odkaz:
http://arxiv.org/abs/2406.01816
Autor:
Sumitani, Rafael, Amorim, João Victor, Mafra, Augusto, Crepalde, Mirlaine, Pereira, Fernando Magno Quintão
Electronic Design Automation (EDA) tools are software applications used by engineers in the design, development, simulation, and verification of electronic systems and integrated circuits. These tools typically process specifications written in a Har
Externí odkaz:
http://arxiv.org/abs/2406.06550
Autor:
Zhang, Tesla, Isaev, Valery
We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax of higher inductive types in homotopy type theory, while coconditions
Externí odkaz:
http://arxiv.org/abs/2405.12994
Autor:
Hivert, Florent, Thiéry, Nicolas M.
Publikováno v:
Order, 07/2022, pages 1-16
C3 is an algorithm used by several widely used programming languages such as Python to support multiple inheritance in object oriented programming (OOP): for each class, C3 computes recursively a linear extension of the poset of all its super classes
Externí odkaz:
http://arxiv.org/abs/2401.12740
Autor:
Chen, Tianyu, Siek, Jeremy G.
Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual languages should satisfy the gradual guarantee: programs that only differ in the precision of their type annotations should behav
Externí odkaz:
http://arxiv.org/abs/2312.02359
Autor:
Zhang, Tesla
The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type theory or cubical type theory. This article describes these application
Externí odkaz:
http://arxiv.org/abs/2311.05658
Autor:
Zhang, Tesla
The conventional general syntax of indexed families in dependent type theories follow the style of "constructors returning a special case", as in Agda, Lean, Idris, Coq, and probably many other systems. Fording is a method to encode indexed families
Externí odkaz:
http://arxiv.org/abs/2309.14187
C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources; dynamic properties of objects and the way they evolve during p
Externí odkaz:
http://arxiv.org/abs/2302.05331