-
Abstract Interpretation-Based Data Leakage Static Analysis
Authors:
Filip Drobnjaković,
Pavle Subotić,
Caterina Urban
Abstract:
Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using run-time metho…
▽ More
Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using run-time methods. However, due to the insidious nature of data leakage, it may not be apparent to a data scientist that a data leakage has occurred in the first place. For this reason, it is advantageous to detect data leakages as early as possible in the development life cycle. In this paper, we propose a novel static analysis to detect several instances of data leakages during development time. We define our analysis using the framework of abstract interpretation: we define a concrete semantics that is sound and complete, from which we derive a sound and computable abstract semantics. We implement our static analysis inside the open-source NBLyzer static analysis framework and demonstrate its utility by evaluating its performance and precision on over 2000 Kaggle competition notebooks.
△ Less
Submitted 29 November, 2022;
originally announced November 2022.
-
Abstract Interpretation-Based Feature Importance for SVMs
Authors:
Abhinandan Pal,
Francesco Ranzato,
Caterina Urban,
Marco Zanella
Abstract:
We propose a symbolic representation for support vector machines (SVMs) by means of abstract interpretation, a well-known and successful technique for designing and implementing static program analyses. We leverage this abstraction in two ways: (1) to enhance the interpretability of SVMs by deriving a novel feature importance measure, called abstract feature importance (AFI), that does not depend…
▽ More
We propose a symbolic representation for support vector machines (SVMs) by means of abstract interpretation, a well-known and successful technique for designing and implementing static program analyses. We leverage this abstraction in two ways: (1) to enhance the interpretability of SVMs by deriving a novel feature importance measure, called abstract feature importance (AFI), that does not depend in any way on a given dataset of the accuracy of the SVM and is very fast to compute, and (2) for verifying stability, notably individual fairness, of SVMs and producing concrete counterexamples when the verification fails. We implemented our approach and we empirically demonstrated its effectiveness on SVMs based on linear and non-linear (polynomial and radial basis function) kernels. Our experimental results show that, independently of the accuracy of the SVM, our AFI measure correlates much more strongly with the stability of the SVM to feature perturbations than feature importance measures widely available in machine learning software such as permutation feature importance. It thus gives better insight into the trustworthiness of SVMs.
△ Less
Submitted 22 October, 2022;
originally announced October 2022.
-
Verifying Attention Robustness of Deep Neural Networks against Semantic Perturbations
Authors:
Satoshi Munakata,
Caterina Urban,
Haruki Yokoyama,
Koji Yamamoto,
Kazuki Munakata
Abstract:
It is known that deep neural networks (DNNs) classify an input image by paying particular attention to certain specific pixels; a graphical representation of the magnitude of attention to each pixel is called a saliency-map. Saliency-maps are used to check the validity of the classification decision basis, e.g., it is not a valid basis for classification if a DNN pays more attention to the backgro…
▽ More
It is known that deep neural networks (DNNs) classify an input image by paying particular attention to certain specific pixels; a graphical representation of the magnitude of attention to each pixel is called a saliency-map. Saliency-maps are used to check the validity of the classification decision basis, e.g., it is not a valid basis for classification if a DNN pays more attention to the background rather than the subject of an image. Semantic perturbations can significantly change the saliency-map. In this work, we propose the first verification method for attention robustness, i.e., the local robustness of the changes in the saliency-map against combinations of semantic perturbations. Specifically, our method determines the range of the perturbation parameters (e.g., the brightness change) that maintains the difference between the actual saliency-map change and the expected saliency-map change below a given threshold value. Our method is based on activation region traversals, focusing on the outermost robust boundary for scalability on larger DNNs. Experimental results demonstrate that our method can show the extent to which DNNs can classify with the same basis regardless of semantic perturbations and report on performance and performance factors of activation region traversals.
△ Less
Submitted 12 July, 2022;
originally announced July 2022.
-
Deep Learning-Based Estimation and Goodness-of-Fit for Large-Scale Confirmatory Item Factor Analysis
Authors:
Christopher J. Urban,
Daniel J. Bauer
Abstract:
We investigate novel parameter estimation and goodness-of-fit (GOF) assessment methods for large-scale confirmatory item factor analysis (IFA) with many respondents, items, and latent factors. For parameter estimation, we extend Urban and Bauer's (2021) deep learning algorithm for exploratory IFA to the confirmatory setting by showing how to handle constraints on loadings and factor correlations.…
▽ More
We investigate novel parameter estimation and goodness-of-fit (GOF) assessment methods for large-scale confirmatory item factor analysis (IFA) with many respondents, items, and latent factors. For parameter estimation, we extend Urban and Bauer's (2021) deep learning algorithm for exploratory IFA to the confirmatory setting by showing how to handle constraints on loadings and factor correlations. For GOF assessment, we explore simulation-based tests and indices that extend the classifier two-sample test (C2ST), a method that tests whether a deep neural network can distinguish between observed data and synthetic data sampled from a fitted IFA model. Proposed extensions include a test of approximate fit wherein the user specifies what percentage of observed and synthetic data should be distinguishable as well as a relative fit index (RFI) that is similar in spirit to the RFIs used in structural equation modeling. Via simulation studies, we show that: (1) the confirmatory extension of Urban and Bauer's (2021) algorithm obtains comparable estimates to a state-of-the-art estimation procedure in less time; (2) C2ST-based GOF tests control the empirical type I error rate and detect when the latent dimensionality is misspecified; and (3) the sampling distribution of the C2ST-based RFI depends on the sample size.
△ Less
Submitted 15 March, 2023; v1 submitted 20 September, 2021;
originally announced September 2021.
-
A Review of Formal Methods applied to Machine Learning
Authors:
Caterina Urban,
Antoine Miné
Abstract:
We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certificati…
▽ More
We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems that include machine learning has only been considered recently and poses novel challenges in soundness, precision, and scalability.
We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software, with a focus on abstract interpretation based techniques as they provide a high level of scalability. This provides a golden standard and sets high expectations for machine learning verification. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations. The large majority of them verify trained neural networks and employ either SMT, optimization, or abstract interpretation techniques. We also discuss methods for support vector machines and decision tree ensembles, as well as methods targeting training and data preparation, which are critical but often neglected aspects of machine learning. Finally, we offer perspectives for future research directions towards the formal verification of machine learning systems.
△ Less
Submitted 21 April, 2021; v1 submitted 6 April, 2021;
originally announced April 2021.
-
Fair Training of Decision Tree Classifiers
Authors:
Francesco Ranzato,
Caterina Urban,
Marco Zanella
Abstract:
We study the problem of formally verifying individual fairness of decision tree ensembles, as well as training tree models which maximize both accuracy and individual fairness. In our approach, fairness verification and fairness-aware training both rely on a notion of stability of a classification model, which is a variant of standard robustness under input perturbations used in adversarial machin…
▽ More
We study the problem of formally verifying individual fairness of decision tree ensembles, as well as training tree models which maximize both accuracy and individual fairness. In our approach, fairness verification and fairness-aware training both rely on a notion of stability of a classification model, which is a variant of standard robustness under input perturbations used in adversarial machine learning. Our verification and training methods leverage abstract interpretation, a well established technique for static program analysis which is able to automatically infer assertions about stability properties of decision trees. By relying on a tool for adversarial training of decision trees, our fairness-aware learning method has been implemented and experimentally evaluated on the reference datasets used to assess fairness properties. The experimental results show that our approach is able to train tree models exhibiting a high degree of individual fairness w.r.t. the natural state-of-the-art CART trees and random forests. Moreover, as a by-product, these fair decision trees turn out to be significantly compact, thus enhancing the interpretability of their fairness properties.
△ Less
Submitted 4 January, 2021;
originally announced January 2021.
-
What Programs Want: Automatic Inference of Input Data Specifications
Authors:
Caterina Urban
Abstract:
Nowadays, as machine-learned software quickly permeates our society, we are becoming increasingly vulnerable to programming errors in the data pre-processing or training software, as well as errors in the data itself. In this paper, we propose a static shape analysis framework for input data of data-processing programs. Our analysis automatically infers necessary conditions on the structure and va…
▽ More
Nowadays, as machine-learned software quickly permeates our society, we are becoming increasingly vulnerable to programming errors in the data pre-processing or training software, as well as errors in the data itself. In this paper, we propose a static shape analysis framework for input data of data-processing programs. Our analysis automatically infers necessary conditions on the structure and values of the data read by a data-processing program. Our framework builds on a family of underlying abstract domains, extended to indirectly reason about the input data rather than simply reasoning about the program variables. The choice of these abstract domain is a parameter of the analysis. We describe various instances built from existing abstract domains. The proposed approach is implemented in an open-source static analyzer for Python programs. We demonstrate its potential on a number of representative examples.
△ Less
Submitted 21 July, 2020;
originally announced July 2020.
-
A Deep Learning Algorithm for High-Dimensional Exploratory Item Factor Analysis
Authors:
Christopher J. Urban,
Daniel J. Bauer
Abstract:
Marginal maximum likelihood (MML) estimation is the preferred approach to fitting item response theory models in psychometrics due to the MML estimator's consistency, normality, and efficiency as the sample size tends to infinity. However, state-of-the-art MML estimation procedures such as the Metropolis-Hastings Robbins-Monro (MH-RM) algorithm as well as approximate MML estimation procedures such…
▽ More
Marginal maximum likelihood (MML) estimation is the preferred approach to fitting item response theory models in psychometrics due to the MML estimator's consistency, normality, and efficiency as the sample size tends to infinity. However, state-of-the-art MML estimation procedures such as the Metropolis-Hastings Robbins-Monro (MH-RM) algorithm as well as approximate MML estimation procedures such as variational inference (VI) are computationally time-consuming when the sample size and the number of latent factors are very large. In this work, we investigate a deep learning-based VI algorithm for exploratory item factor analysis (IFA) that is computationally fast even in large data sets with many latent factors. The proposed approach applies a deep artificial neural network model called an importance-weighted autoencoder (IWAE) for exploratory IFA. The IWAE approximates the MML estimator using an importance sampling technique wherein increasing the number of importance-weighted (IW) samples drawn during fitting improves the approximation, typically at the cost of decreased computational efficiency. We provide a real data application that recovers results aligning with psychological theory across random starts. Via simulation studies, we show that the IWAE yields more accurate estimates as either the sample size or the number of IW samples increases (although factor correlation and intercepts estimates exhibit some bias) and obtains similar results to MH-RM in less time. Our simulations also suggest that the proposed approach performs similarly to and is potentially faster than constrained joint maximum likelihood estimation, a fast procedure that is consistent when the sample size and the number of items simultaneously tend to infinity.
△ Less
Submitted 4 February, 2021; v1 submitted 21 January, 2020;
originally announced January 2020.
-
Perfectly Parallel Fairness Certification of Neural Networks
Authors:
Caterina Urban,
Maria Christakis,
Valentin Wüstholz,
Fuyuan Zhang
Abstract:
Recently, there is growing concern that machine-learning models, which currently assist or even automate decision making, reproduce, and in the worst case reinforce, bias of the training data. The development of tools and techniques for certifying fairness of these models or describing their biased behavior is, therefore, critical. In this paper, we propose a perfectly parallel static analysis for…
▽ More
Recently, there is growing concern that machine-learning models, which currently assist or even automate decision making, reproduce, and in the worst case reinforce, bias of the training data. The development of tools and techniques for certifying fairness of these models or describing their biased behavior is, therefore, critical. In this paper, we propose a perfectly parallel static analysis for certifying causal fairness of feed-forward neural networks used for classification of tabular data. When certification succeeds, our approach provides definite guarantees, otherwise, it describes and quantifies the biased behavior. We design the analysis to be sound, in practice also exact, and configurable in terms of scalability and precision, thereby enabling pay-as-you-go certification. We implement our approach in an open-source tool and demonstrate its effectiveness on models trained with popular datasets.
△ Less
Submitted 21 April, 2020; v1 submitted 5 December, 2019;
originally announced December 2019.
-
Permission Inference for Array Programs
Authors:
Jérôme Dohrau,
Alexander J. Summers,
Caterina Urban,
Severin Münger,
Peter Müller
Abstract:
Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission…
▽ More
Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools. Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination. Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops.
△ Less
Submitted 11 April, 2018;
originally announced April 2018.
-
Low vibration high numerical aperture automated variable temperature Raman microscope
Authors:
Yao Tian,
Anjan A. Reijnders,
Gavin B. Osterhoudt,
Ilya Valmianski,
J. G. Ramirez,
Christian Urban,
Ruidan Zhong,
John Schneeloch,
Genda Gu,
Isaac Henslee,
Kenneth S. Burch
Abstract:
Raman micro-spectroscopy is well suited for studying a variety of properties and has been applied to wide- ranging areas. Combined with tuneable temperature, Raman spectra can offer even more insights into the properties of materials. However, previous designs of variable temperature Raman microscopes have made it extremely challenging to measure samples with low signal levels due to thermal and p…
▽ More
Raman micro-spectroscopy is well suited for studying a variety of properties and has been applied to wide- ranging areas. Combined with tuneable temperature, Raman spectra can offer even more insights into the properties of materials. However, previous designs of variable temperature Raman microscopes have made it extremely challenging to measure samples with low signal levels due to thermal and positional instability as well as low collection efficiencies. Thus, contemporary Raman microscope has found limited applicability to probing the subtle physics involved in phase transitions and hysteresis. This paper describes a new design of a closed-cycle, Raman microscope with full polarization rotation. High collection efficiency, thermal and mechanical stability are ensured by both deliberate optical, cryogenic, and mechanical design. Measurements on two samples, Bi2Se3 and V2O3, which are known as challenging due to low thermal conductivities, low signal levels and/or hysteretic effects, are measured with previously undemonstrated temperature resolution.
△ Less
Submitted 8 April, 2016;
originally announced April 2016.
-
Modelling homogeneous generative meta-programming
Authors:
Martin Berger,
Laurence Tratt,
Christian Urban
Abstract:
Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present the first foundational calculus which can model powerful HGMP languages such as Template Haskell. The calculus is designed such that we can gradually enhance it with the features needed to model many of the advanced features of real languages. As a demonstration of the…
▽ More
Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present the first foundational calculus which can model powerful HGMP languages such as Template Haskell. The calculus is designed such that we can gradually enhance it with the features needed to model many of the advanced features of real languages. As a demonstration of the flexibility of our approach, we also provide a simple type system for the calculus.
△ Less
Submitted 23 April, 2017; v1 submitted 21 February, 2016;
originally announced February 2016.
-
Synthetic magnetoelectric coupling in a nanocomposite multiferroic
Authors:
P. Jain,
Q. Wang,
M. Roldan,
A. Glavic,
V. Lauter,
C. Urban,
Z. Bi,
T. Ahmed,
J. Zhu,
M. Varela,
Q. Jia,
M. R. Fitzsimmons
Abstract:
Given the paucity of single phase multiferroic materials (with large ferromagnetic moment), composite systems seem an attractive solution in the quest to realize magnetoelectric cou-pling between ferromagnetic and ferroelectric order parameters. Despite having antiferro-magnetic order, BiFeO3 (BFO) has nevertheless been a key material in this quest due to excel-lent ferroelectric properties at roo…
▽ More
Given the paucity of single phase multiferroic materials (with large ferromagnetic moment), composite systems seem an attractive solution in the quest to realize magnetoelectric cou-pling between ferromagnetic and ferroelectric order parameters. Despite having antiferro-magnetic order, BiFeO3 (BFO) has nevertheless been a key material in this quest due to excel-lent ferroelectric properties at room temperature. We studied a superlattice composed of 8 repetitions of 6 unit cells of La0.7Sr0.3MnO3 (LSMO) grown on 5 unit cells of BFO. Significant net uncompensated magnetization in BFO is demonstrated using polarized neutron reflectometry in an insulating superlattice. Remarkably, the magnetization enables magnetic field to change the dielectric properties of the superlattice, which we cite as an example of synthetic magnetoelectric coupling. Importantly, this controlled creation of magnetic moment in BFO suggests a much needed path forward for the design and implementation of integrated oxide devices for next generation magnetoelectric data storage platforms.
△ Less
Submitted 11 September, 2014; v1 submitted 30 July, 2014;
originally announced July 2014.
-
General Bindings and Alpha-Equivalence in Nominal Isabelle
Authors:
Christian Urban,
Cezary Kaliszyk
Abstract:
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means term constructors where multiple variables are bound at once.…
▽ More
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means term constructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. Our extension includes new definitions of alpha-equivalence and establishes automatically the reasoning infrastructure for alpha-equated terms. We also prove strong induction principles that have the usual variable convention already built in.
△ Less
Submitted 19 June, 2012; v1 submitted 1 June, 2012;
originally announced June 2012.
-
Nominal Unification Revisited
Authors:
Christian Urban
Abstract:
Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as the use of first-order terms with names (as opposed to alpha-equivalence classes) and that no new names need to be generated during unification, which set it…
▽ More
Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as the use of first-order terms with names (as opposed to alpha-equivalence classes) and that no new names need to be generated during unification, which set it clearly apart from higher-order pattern unification. The purpose of this paper is to simplify a clunky proof from the original paper on nominal unification and to give an overview over some results about nominal unification.
△ Less
Submitted 22 December, 2010;
originally announced December 2010.
-
Fabrication method for micro vapor cells for alkali atoms
Authors:
T. Baluktsian,
C. Urban,
T. Bublat,
H. Giessen,
R. Löw,
T. Pfau
Abstract:
A quantum network which consists of several components should ideally work on a single physical platform. Neutral alkali atoms have the potential to be very well suited for this purpose due to their electronic structure which involves long lived nuclear spins and very sensitive highly excited Rydberg states. In this paper we describe a fabrication method based on quartz glass to structure arbitr…
▽ More
A quantum network which consists of several components should ideally work on a single physical platform. Neutral alkali atoms have the potential to be very well suited for this purpose due to their electronic structure which involves long lived nuclear spins and very sensitive highly excited Rydberg states. In this paper we describe a fabrication method based on quartz glass to structure arbitrary shapes of microscopic vapor cells. We show that the usual spectroscopic properties known from macroscopic vapor cells are almost unaffected by the strong confinement.
△ Less
Submitted 5 February, 2010;
originally announced February 2010.
-
Expected Performance of the ATLAS Experiment - Detector, Trigger and Physics
Authors:
The ATLAS Collaboration,
G. Aad,
E. Abat,
B. Abbott,
J. Abdallah,
A. A. Abdelalim,
A. Abdesselam,
O. Abdinov,
B. Abi,
M. Abolins,
H. Abramowicz,
B. S. Acharya,
D. L. Adams,
T. N. Addy,
C. Adorisio,
P. Adragna,
T. Adye,
J. A. Aguilar-Saavedra,
M. Aharrouche,
S. P. Ahlen,
F. Ahles,
A. Ahmad,
H. Ahmed,
G. Aielli,
T. Akdogan
, et al. (2587 additional authors not shown)
Abstract:
A detailed study is presented of the expected performance of the ATLAS detector. The reconstruction of tracks, leptons, photons, missing energy and jets is investigated, together with the performance of b-tagging and the trigger. The physics potential for a variety of interesting physics processes, within the Standard Model and beyond, is examined. The study comprises a series of notes based on…
▽ More
A detailed study is presented of the expected performance of the ATLAS detector. The reconstruction of tracks, leptons, photons, missing energy and jets is investigated, together with the performance of b-tagging and the trigger. The physics potential for a variety of interesting physics processes, within the Standard Model and beyond, is examined. The study comprises a series of notes based on simulations of the detector and physics processes, with particular emphasis given to the data expected from the first years of operation of the LHC at CERN.
△ Less
Submitted 14 August, 2009; v1 submitted 28 December, 2008;
originally announced January 2009.
-
Mechanizing the Metatheory of LF
Authors:
Christian Urban,
James Cheney,
Stefan Berghofer
Abstract:
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized th…
▽ More
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized these properties within Isabelle/HOL using the Nominal Datatype Package, closely following a recent article by Harper and Pfenning. In the process, we identified and resolved a gap in one of the proofs and a small number of minor lacunae in others. We also formally derive a version of the type checking algorithm from which Isabelle/HOL can generate executable code. Besides its intrinsic interest, our formalization provides a foundation for studying the adequacy of LF encodings, the correctness of Twelf-style metatheoretic reasoning, and the metatheory of extensions to LF.
△ Less
Submitted 3 May, 2010; v1 submitted 10 April, 2008;
originally announced April 2008.
-
Nominal Logic Programming
Authors:
James Cheney,
Christian Urban
Abstract:
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational seman…
▽ More
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via examples.
△ Less
Submitted 20 August, 2007; v1 submitted 12 September, 2006;
originally announced September 2006.