Nominal techniques

Last updated

Nominal techniques in computer science are a range of techniques, based on nominal sets, for handling names and binding, e.g. in abstract syntax. Research into nominal sets gave rise to nominal terms, a metalanguage for embedding object languages with name binding constructs.

See also

Related Research Articles

In computing, a compiler is a computer program that translates computer code written in one programming language into another language. The name "compiler" is primarily used for programs that translate source code from a high-level programming language to a lower level language to create an executable program.

Prolog is a logic programming language associated with artificial intelligence and computational linguistics.

Scheme (programming language) Dialect of Lisp

Scheme is a minimalist dialect of the Lisp family of programming languages. Scheme consists of a small standard core with several tools for language extension.

In computer science, denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.

In software engineering and computer science, abstraction is:

Neurolinguistics Neuroscience- and linguistics-related studies

Neurolinguistics is the study of the neural mechanisms in the human brain that control the comprehension, production, and acquisition of language. As an interdisciplinary field, neurolinguistics draws methods and theories from fields such as neuroscience, linguistics, cognitive science, communication disorders and neuropsychology. Researchers are drawn to the field from a variety of backgrounds, bringing along a variety of experimental techniques as well as widely varying theoretical perspectives. Much work in neurolinguistics is informed by models in psycholinguistics and theoretical linguistics, and is focused on investigating how the brain can implement the processes that theoretical and psycholinguistics propose are necessary in producing and comprehending language. Neurolinguists study the physiological mechanisms by which the brain processes information related to language, and evaluate linguistic and psycholinguistic theories, using aphasiology, brain imaging, electrophysiology, and computer modeling.

The Web Ontology Language (OWL) is a family of knowledge representation languages for authoring ontologies. Ontologies are a formal way to describe taxonomies and classification networks, essentially defining the structure of knowledge for various domains: the nouns representing classes of objects and the verbs representing relations between the objects.

Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970.

In computer science, an abstract semantic graph (ASG) or term graph is a form of abstract syntax in which an expression of a formal or programming language is represented by a graph whose vertices are the expression's subterms. An ASG is at a higher level of abstraction than an abstract syntax tree, which is used to express the syntactic structure of an expression or program.

Docking (molecular)

In the field of molecular modeling, docking is a method which predicts the preferred orientation of one molecule to a second when a lingand and a target are bound to each other to form a stable complex. Knowledge of the preferred orientation in turn may be used to predict the strength of association or binding affinity between two molecules using, for example, scoring functions.

In computer science, higher-order abstract syntax is a technique for the representation of abstract syntax trees for languages with variable binders.

In computer science, Programming Computable Functions (PCF) is a typed functional language introduced by Gordon Plotkin in 1977, based on previous unpublished material by Dana Scott. It can be considered to be an extended version of the typed lambda calculus or a simplified version of modern typed functional languages such as ML or Haskell.

Dov M. Gabbay is an Israeli logician. He is Augustus De Morgan Professor Emeritus of Logic at the Group of Logic, Language and Computation, Department of Computer Science, King's College London.

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

In mathematical logic, the De Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables. Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality. Each De Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples:

In mathematical logic and computer science, Gabbay's separation theorem, named after Dov Gabbay, states that any arbitrary temporal logic formula can be rewritten in a logically equivalent "past → future" form. I.e. the future becomes what must be satisfied. This form can be used as execution rules; a MetateM program is a set of such rules.

Aldo-keto reductase

The aldo-keto reductase family is a family of proteins that are subdivided into 16 categories; these include a number of related monomeric NADPH-dependent oxidoreductases, such as aldehyde reductase, aldose reductase, prostaglandin F synthase, xylose reductase, rho crystallin, and many others.

Nominal terms are a metalanguage for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence. Nominal terms came out of a programme of research into nominal sets, and have a concrete semantics in those sets.

Ruy de Queiroz

Ruy J. Guerra B. de Queiroz is an associate professor at Universidade Federal de Pernambuco and holds significant works in the research fields of Mathematical logic, proof theory, foundations of mathematics and philosophy of mathematics. He is the founder of the Workshop on Logic, Language, Information and Computation (WoLLIC), which has been organised annually since 1994, typically in June or July.

ACM SIGLOG or SIGLOG is the Association for Computing Machinery Special Interest Group on Logic and Computation. It publishes a news magazine, and has the annual Symposium on Logic in Computer Science as its flagship conference. In addition, it publishes an online newsletter, the SIGLOG Monthly Bulletin, and "maintains close ties" with the related academic journal ACM Transactions on Computational Logic.

References