-
Additive Multi-Index Gaussian process modeling, with application to multi-physics surrogate modeling of the quark-gluon plasma
Authors:
Kevin Li,
Simon Mak,
J. -F Paquet,
Steffen A. Bass
Abstract:
The Quark-Gluon Plasma (QGP) is a unique phase of nuclear matter, theorized to have filled the Universe shortly after the Big Bang. A critical challenge in studying the QGP is that, to reconcile experimental observables with theoretical parameters, one requires many simulation runs of a complex physics model over a high-dimensional parameter space. Each run is computationally very expensive, requi…
▽ More
The Quark-Gluon Plasma (QGP) is a unique phase of nuclear matter, theorized to have filled the Universe shortly after the Big Bang. A critical challenge in studying the QGP is that, to reconcile experimental observables with theoretical parameters, one requires many simulation runs of a complex physics model over a high-dimensional parameter space. Each run is computationally very expensive, requiring thousands of CPU hours, thus limiting physicists to only several hundred runs. Given limited training data for high-dimensional prediction, existing surrogate models often yield poor predictions with high predictive uncertainties, leading to imprecise scientific findings. To address this, we propose a new Additive Multi-Index Gaussian process (AdMIn-GP) model, which leverages a flexible additive structure on low-dimensional embeddings of the parameter space. This is guided by prior scientific knowledge that the QGP is dominated by multiple distinct physical phenomena (i.e., multiphysics), each involving a small number of latent parameters. The AdMIn-GP models for such embedded structures within a flexible Bayesian nonparametric framework, which facilitates efficient model fitting via a carefully constructed variational inference approach with inducing points. We show the effectiveness of the AdMIn-GP via a suite of numerical experiments and our QGP application, where we demonstrate considerably improved surrogate modeling performance over existing models.
△ Less
Submitted 10 June, 2023;
originally announced June 2023.
-
Learning Flight Control Systems from Human Demonstrations and Real-Time Uncertainty-Informed Interventions
Authors:
Prashant Ganesh,
J. Humberto Ramos,
Vinicius G. Goecks,
Jared Paquet,
Matthew Longmire,
Nicholas R. Waytowich,
Kevin Brink
Abstract:
This paper describes a methodology for learning flight control systems from human demonstrations and interventions while considering the estimated uncertainty in the learned models. The proposed approach uses human demonstrations to train an initial model via imitation learning and then iteratively, improve its performance by using real-time human interventions. The aim of the interventions is to…
▽ More
This paper describes a methodology for learning flight control systems from human demonstrations and interventions while considering the estimated uncertainty in the learned models. The proposed approach uses human demonstrations to train an initial model via imitation learning and then iteratively, improve its performance by using real-time human interventions. The aim of the interventions is to correct undesired behaviors and adapt the model to changes in the task dynamics. The learned model uncertainty is estimated in real-time via Monte Carlo Dropout and the human supervisor is cued for intervention via an audiovisual signal when this uncertainty exceeds a predefined threshold. This proposed approach is validated in an autonomous quadrotor landing task on both fixed and moving platforms. It is shown that with this algorithm, a human can rapidly teach a flight task to an unmanned aerial vehicle via demonstrating expert trajectories and then adapt the learned model by intervening when the learned controller performs any undesired maneuver, the task changes, and/or the model uncertainty exceeds a threshold
△ Less
Submitted 1 May, 2023;
originally announced May 2023.
-
Astronomical image time series classification using CONVolutional attENTION (ConvEntion)
Authors:
Anass Bairouk,
Marc Chaumont,
Dominique Fouchez,
Jerome Paquet,
Frédéric Comby,
Julian Bautista
Abstract:
Aims. The treatment of astronomical image time series has won increasing attention in recent years. Indeed, numerous surveys following up on transient objects are in progress or under construction, such as the Vera Rubin Observatory Legacy Survey for Space and Time (LSST), which is poised to produce huge amounts of these time series. The associated scientific topics are extensive, ranging from the…
▽ More
Aims. The treatment of astronomical image time series has won increasing attention in recent years. Indeed, numerous surveys following up on transient objects are in progress or under construction, such as the Vera Rubin Observatory Legacy Survey for Space and Time (LSST), which is poised to produce huge amounts of these time series. The associated scientific topics are extensive, ranging from the study of objects in our galaxy to the observation of the most distant supernovae for measuring the expansion of the universe. With such a large amount of data available, the need for robust automatic tools to detect and classify celestial objects is growing steadily. Methods. This study is based on the assumption that astronomical images contain more information than light curves. In this paper, we propose a novel approach based on deep learning for classifying different types of space objects directly using images. We named our approach ConvEntion, which stands for CONVolutional attENTION. It is based on convolutions and transformers, which are new approaches for the treatment of astronomical image time series. Our solution integrates spatio-temporal features and can be applied to various types of image datasets with any number of bands. Results. In this work, we solved various problems the datasets tend to suffer from and we present new results for classifications using astronomical image time series with an increase in accuracy of 13%, compared to state-of-the-art approaches that use image time series, and a 12% increase, compared to approaches that use light curves.
△ Less
Submitted 3 April, 2023;
originally announced April 2023.
-
Toward Multimodal Interaction in Scalable Visual Digital Evidence Visualization Using Computer Vision Techniques and ISS
Authors:
Serguei A. Mokhov,
Miao Song,
Jashanjot Singh,
Joey Paquet,
Mourad Debbabi,
Sudhir Mudur
Abstract:
Visualization requirements in Forensic Lucid have to do with different levels of case knowledge abstraction, representation, aggregation, as well as the operational aspects as the final long-term goal of this proposal. It encompasses anything from the finer detailed representation of hierarchical contexts to Forensic Lucid programs, to the documented evidence and its management, its linkage to pro…
▽ More
Visualization requirements in Forensic Lucid have to do with different levels of case knowledge abstraction, representation, aggregation, as well as the operational aspects as the final long-term goal of this proposal. It encompasses anything from the finer detailed representation of hierarchical contexts to Forensic Lucid programs, to the documented evidence and its management, its linkage to programs, to evaluation, and to the management of GIPSY software networks. This includes an ability to arbitrarily switch between those views combined with usable multimodal interaction. The purpose is to determine how the findings can be applied to Forensic Lucid and investigation case management. It is also natural to want a convenient and usable evidence visualization, its semantic linkage and the reasoning machinery for it. Thus, we propose a scalable management, visualization, and evaluation of digital evidence using the modified interactive 3D documentary system - Illimitable Space System - (ISS) to represent, semantically link, and provide a usable interface to digital investigators that is navigable via different multimodal interaction techniques using Computer Vision techniques including gestures, as well as eye-gaze and audio.
△ Less
Submitted 31 July, 2018;
originally announced August 2018.
-
Fast Context-Annotated Classification of Different Types of Web Service Descriptions
Authors:
Serguei A. Mokhov,
Joey Paquet,
Arash Khodadadi
Abstract:
In the recent rapid growth of web services, IoT, and cloud computing, many web services and APIs appeared on the web. With the failure of global UDDI registries, different service repositories started to appear, trying to list and categorize various types of web services for client applications' discover and use. In order to increase the effectiveness and speed up the task of finding compatible We…
▽ More
In the recent rapid growth of web services, IoT, and cloud computing, many web services and APIs appeared on the web. With the failure of global UDDI registries, different service repositories started to appear, trying to list and categorize various types of web services for client applications' discover and use. In order to increase the effectiveness and speed up the task of finding compatible Web Services in the brokerage when performing service composition or suggesting Web Services to the requests, high-level functionality of the service needs to be determined. Due to the lack of structured support for specifying such functionality, classification of services into a set of abstract categories is necessary. We employ a wide range of Machine Learning and Signal Processing algorithms and techniques in order to find the highest precision achievable in the scope of this article for the fast classification of three type of service descriptions: WSDL, REST, and WADL. In addition, we complement our approach by showing the importance and effect of contextual information on the classification of the service descriptions and show that it improves the accuracy in 5 different categories of services.
△ Less
Submitted 31 May, 2018;
originally announced June 2018.
-
An Interactive Graph-Based Automation Assistant: A Case Study to Manage the GIPSY's Distributed Multi-tier Run-Time System
Authors:
Sleiman Rabah,
Serguei A. Mokhov,
Joey Paquet
Abstract:
The GIPSY system provides a framework for a distributed multi-tier demand-driven evaluation of heterogeneous programs, in which certain tiers can generate demands, while others can respond to demands to work on them. They are connected through a virtual network that can be flexibly reconfigured at run-time. Although the demand generator components were originally designed specifically for the educ…
▽ More
The GIPSY system provides a framework for a distributed multi-tier demand-driven evaluation of heterogeneous programs, in which certain tiers can generate demands, while others can respond to demands to work on them. They are connected through a virtual network that can be flexibly reconfigured at run-time. Although the demand generator components were originally designed specifically for the eductive (demand-driven) evaluation of Lucid intensional programs, the GIPSY's run-time's flexible framework design enables it to perform the execution of various kinds of programs that can be evaluated using the demand-driven computational model. Management of the GISPY networks has become a tedious (although scripted) task that took manual command-line console to do, which does not scale for large experiments. Therefore a new component has been designed and developed to allow users to represent, visualize, and interactively create, configure and seamlessly manage such a network as a graph. Consequently, this work presents a Graphical GMT Manager, an interactive graph-based assistant component for the GIPSY network creation and configuration management. Besides allowing the management of the nodes and tiers (mapped to hosts where store, workers, and generators reside), it lets the user to visually control the network parameters and the interconnection between computational nodes at run-time. In this paper we motivate and present the key features of this newly implemented graph-based component. We give the graph representation details, map** of the graph nodes to tiers, tier groups, and specific commands. We provide the requirements and design specification of the tool and its implementation. Then we detail and discuss some experimental results.
△ Less
Submitted 21 June, 2013; v1 submitted 17 December, 2012;
originally announced December 2012.
-
MARFCAT: Transitioning to Binary and Larger Data Sets of SATE IV
Authors:
Serguei A. Mokhov,
Joey Paquet,
Mourad Debbabi,
Yankui Sun
Abstract:
We present a second iteration of a machine learning approach to static code analysis and fingerprinting for weaknesses related to security, software engineering, and others using the open-source MARF framework and the MARFCAT application based on it for the NIST's SATE IV static analysis tool exposition workshop's data sets that include additional test cases, including new large synthetic cases. T…
▽ More
We present a second iteration of a machine learning approach to static code analysis and fingerprinting for weaknesses related to security, software engineering, and others using the open-source MARF framework and the MARFCAT application based on it for the NIST's SATE IV static analysis tool exposition workshop's data sets that include additional test cases, including new large synthetic cases. To aid detection of weak or vulnerable code, including source or binary on different platforms the machine learning approach proved to be fast and accurate to for such tasks where other tools are either much slower or have much smaller recall of known vulnerabilities. We use signal and NLP processing techniques in our approach to accomplish the identification and classification tasks. MARFCAT's design from the beginning in 2010 made is independent of the language being analyzed, source code, bytecode, or binary. In this follow up work with explore some preliminary results in this area. We evaluated also additional algorithms that were used to process the data.
△ Less
Submitted 10 May, 2013; v1 submitted 16 July, 2012;
originally announced July 2012.
-
Furthering Baseline Core Lucid Standard Specification in the Context of the History of Lucid, Intensional Programming, and Context-Aware Computing
Authors:
Joey Paquet,
Serguei A. Mokhov
Abstract:
This work is multifold. We review the historical literature on the Lucid programming language, its dialects, intensional logic, intensional programming, the implementing systems, and context-oriented and context-aware computing and so on that provide a contextual framework for the converging Core Lucid standard programming model. We are designing a standard specification of a baseline Lucid virtua…
▽ More
This work is multifold. We review the historical literature on the Lucid programming language, its dialects, intensional logic, intensional programming, the implementing systems, and context-oriented and context-aware computing and so on that provide a contextual framework for the converging Core Lucid standard programming model. We are designing a standard specification of a baseline Lucid virtual machine for generic execution of Lucid programs. The resulting Core Lucid language would inherit the properties of generalization attempts of GIPL (1999-2013) and TransLucid (2008-2013) for all future and recent Lucid implementing systems to follow. We also maintain this work across local research group in order to foster deeper collaboration, maintain a list of recent and historical bibliography and a reference manual and reading list for students. We form a (for now informal) SIGLUCID group to keep track of this standard and historical records with eventual long-term goal through iterative revisions for this work to become a book or an encyclopedia of the referenced topics, and perhaps, an RFC. We first begin small with this initial set of notes.
△ Less
Submitted 21 October, 2013; v1 submitted 5 July, 2011;
originally announced July 2011.
-
Towards Refactoring the DMF to Support **i and JMS DMS in GIPSY
Authors:
Yi Ji,
Serguei A. Mokhov,
Joey Paquet
Abstract:
In this paper we report on our re-engineering effort to refactor and unify two somewhat disjoint Java distributed middleware technologies -- **i and JMS -- used in the implementation of the Demand Migration System (DMS). In doing so, we refactor their parent Demand Migration Framework (DMF), within the General Intensional Programming System (GIPSY). The complex Java-based GIPSY project is used to…
▽ More
In this paper we report on our re-engineering effort to refactor and unify two somewhat disjoint Java distributed middleware technologies -- **i and JMS -- used in the implementation of the Demand Migration System (DMS). In doing so, we refactor their parent Demand Migration Framework (DMF), within the General Intensional Programming System (GIPSY). The complex Java-based GIPSY project is used to investigate on the intensional and hybrid programming paradigms.
△ Less
Submitted 3 May, 2011; v1 submitted 13 December, 2010;
originally announced December 2010.
-
The Need to Support of Data Flow Graph Visualization of Forensic Lucid Programs, Forensic Evidence, and their Evaluation by GIPSY
Authors:
Serguei A. Mokhov,
Joey Paquet,
Mourad Debbabi
Abstract:
Lucid programs are data-flow programs and can be visually represented as data flow graphs (DFGs) and composed visually. Forensic Lucid, a Lucid dialect, is a language to specify and reason about cyberforensic cases. It includes the encoding of the evidence (representing the context of evaluation) and the crime scene modeling in order to validate claims against the model and perform event reconstru…
▽ More
Lucid programs are data-flow programs and can be visually represented as data flow graphs (DFGs) and composed visually. Forensic Lucid, a Lucid dialect, is a language to specify and reason about cyberforensic cases. It includes the encoding of the evidence (representing the context of evaluation) and the crime scene modeling in order to validate claims against the model and perform event reconstruction, potentially within large swaths of digital evidence. To aid investigators to model the scene and evaluate it, instead of ty** a Forensic Lucid program, we propose to expand the design and implementation of the Lucid DFG programming onto Forensic Lucid case modeling and specification to enhance the usability of the language and the system and its behavior. We briefly discuss the related work on visual programming an DFG modeling in an attempt to define and select one approach or a composition of approaches for Forensic Lucid based on various criteria such as previous implementation, wide use, formal backing in terms of semantics and translation. In the end, we solicit the readers' constructive, opinions, feedback, comments, and recommendations within the context of this short discussion.
△ Less
Submitted 30 May, 2011; v1 submitted 27 September, 2010;
originally announced September 2010.
-
Comparative Studies of Programming Languages; Course Lecture Notes
Authors:
Joey Paquet,
Serguei A. Mokhov
Abstract:
Lecture notes for the Comparative Studies of Programming Languages course, COMP6411, taught at the Department of Computer Science and Software Engineering, Faculty of Engineering and Computer Science, Concordia University, Montreal, QC, Canada. These notes include a compiled book of primarily related articles from the Wikipedia, the Free Encyclopedia, as well as Comparative Programming Languages b…
▽ More
Lecture notes for the Comparative Studies of Programming Languages course, COMP6411, taught at the Department of Computer Science and Software Engineering, Faculty of Engineering and Computer Science, Concordia University, Montreal, QC, Canada. These notes include a compiled book of primarily related articles from the Wikipedia, the Free Encyclopedia, as well as Comparative Programming Languages book and other resources, including our own. The original notes were compiled by Dr. Paquet.
△ Less
Submitted 4 August, 2010; v1 submitted 12 July, 2010;
originally announced July 2010.
-
Complete Context Calculus Design and Implementation in GIPSY
Authors:
Xin Tong,
Joey Paquet,
Serguei A. Mokhov
Abstract:
This paper presents the integration into the GIPSY of Lucx's context calculus defined in Wan's PhD thesis. We start by defining different types of tag sets, then we explain the concept of context, the types of context and the context calculus operators. Finally, we present how context entities have been abstracted into Java classes and embedded into the GIPSY system.
This paper presents the integration into the GIPSY of Lucx's context calculus defined in Wan's PhD thesis. We start by defining different types of tag sets, then we explain the concept of context, the types of context and the context calculus operators. Finally, we present how context entities have been abstracted into Java classes and embedded into the GIPSY system.
△ Less
Submitted 23 February, 2010;
originally announced February 2010.
-
Object-Oriented Intensional Programming: Intensional Classes Using Java and Lucid
Authors:
Aihua Wu,
Joey Paquet,
Serguei A. Mokhov
Abstract:
This article introduces Object-Oriented Intensional Programming (OO-IP), a new hybrid language between Object-Oriented and Intensional Programming Languages in the sense of the latest evolutions of Lucid. This new hybrid language combines the essential characteristics of Lucid and Java, and introduces the notion of object streams which makes it is possible that each element in a Lucid stream to…
▽ More
This article introduces Object-Oriented Intensional Programming (OO-IP), a new hybrid language between Object-Oriented and Intensional Programming Languages in the sense of the latest evolutions of Lucid. This new hybrid language combines the essential characteristics of Lucid and Java, and introduces the notion of object streams which makes it is possible that each element in a Lucid stream to be an object with embedded intensional properties. Interestingly, this hybrid language also brings to Java objects the power to explicitly express and manipulate the notion of context, creating the novel concept of intensional object, i.e. objects whose evaluation is context-dependent, which are here demonstrated to be translatable into standard objects. By this new approach, we extend the use and meaning of the notion of intensional objects and enrich the meaning of object streams in Lucid and semantics of intensional objects in Java.
△ Less
Submitted 3 September, 2009;
originally announced September 2009.
-
Reasoning About a Simulated Printer Case Investigation with Forensic Lucid
Authors:
Serguei A. Mokhov,
Joey Paquet,
Mourad Debbabi
Abstract:
In this work we model the ACME (a fictitious company name) "printer case incident" and make its specification in Forensic Lucid, a Lucid- and intensional-logic-based programming language for cyberforensic analysis and event reconstruction specification. The printer case involves a dispute between two parties that was previously solved using the finite-state automata (FSA) approach, and is now re-d…
▽ More
In this work we model the ACME (a fictitious company name) "printer case incident" and make its specification in Forensic Lucid, a Lucid- and intensional-logic-based programming language for cyberforensic analysis and event reconstruction specification. The printer case involves a dispute between two parties that was previously solved using the finite-state automata (FSA) approach, and is now re-done in a more usable way in Forensic Lucid. Our simulation is based on the said case modeling by encoding concepts like evidence and the related witness accounts as an evidential statement context in a Forensic Lucid program, which is an input to the transition function that models the possible deductions in the case. We then invoke the transition function (actually its reverse) with the evidential statement context to see if the evidence we encoded agrees with one's claims and then attempt to reconstruct the sequence of events that may explain the claim or disprove it.
△ Less
Submitted 26 April, 2012; v1 submitted 28 June, 2009;
originally announced June 2009.
-
Advances in the Design and Implementation of a Multi-Tier Architecture in the GIPSY Environment
Authors:
Bin Han,
Serguei A. Mokhov,
Joey Paquet
Abstract:
We present advances in the software engineering design and implementation of the multi-tier run-time system for the General Intensional Programming System (GIPSY) by further unifying the distributed technologies used to implement the Demand Migration Framework (DMF) in order to streamline distributed execution of hybrid intensional-imperative programs using Java.
We present advances in the software engineering design and implementation of the multi-tier run-time system for the General Intensional Programming System (GIPSY) by further unifying the distributed technologies used to implement the Demand Migration Framework (DMF) in order to streamline distributed execution of hybrid intensional-imperative programs using Java.
△ Less
Submitted 26 June, 2009;
originally announced June 2009.
-
A Type System Theory for Higher-Order Intensional Logic Support for Variable Bindings in Hybrid Intensional-Imperative Programs in GIPSY
Authors:
Serguei A. Mokhov,
Joey Paquet
Abstract:
We describe a type system for a platform called the General Intensional Programming System (GIPSY), designed to support intensional programming languages built upon intensional logic and their imperative counter-parts for the intensional execution model. In GIPSY, the type system glues the static and dynamic ty** between intensional and imperative languages in its compiler and run-time environ…
▽ More
We describe a type system for a platform called the General Intensional Programming System (GIPSY), designed to support intensional programming languages built upon intensional logic and their imperative counter-parts for the intensional execution model. In GIPSY, the type system glues the static and dynamic ty** between intensional and imperative languages in its compiler and run-time environments to support the intensional evaluation of expressions written in various dialects of the intensional programming language Lucid. The intensionality makes expressions to explicitly take into the account a multidimensional context of evaluation with the context being a first-class value that serves a number of applications that need the notion of context to proceed. We describe and discuss the properties of such a type system and the related type theory as well as particularities of the semantics, design and implementation of the GIPSY type system.
△ Less
Submitted 22 June, 2009;
originally announced June 2009.
-
Using the General Intensional Programming System (GIPSY) for Evaluation of Higher-Order Intensional Logic (HOIL) Expressions
Authors:
Serguei A. Mokhov,
Joey Paquet
Abstract:
The General Intensional Programming System (GIPSY) has been built around the Lucid family of intensional programming languages that rely on the higher-order intensional logic (HOIL) to provide context-oriented multidimensional reasoning of intensional expressions. HOIL combines functional programming with various intensional logics to allow explicit context expressions to be evaluated as first-c…
▽ More
The General Intensional Programming System (GIPSY) has been built around the Lucid family of intensional programming languages that rely on the higher-order intensional logic (HOIL) to provide context-oriented multidimensional reasoning of intensional expressions. HOIL combines functional programming with various intensional logics to allow explicit context expressions to be evaluated as first-class values that can be passed as parameters to functions and return as results with an appropriate set of operators defined on contexts. GIPSY's frameworks are implemented in Java as a collection of replaceable components for the compilers of various Lucid dialects and the demand-driven eductive evaluation engine that can run distributively. GIPSY provides support for hybrid programming models that couple intensional and imperative languages for a variety of needs. Explicit context expressions limit the scope of evaluation of math expressions (effectively a Lucid program is a mathematics or physics expression constrained by the context) in tensor physics, regular math in multiple dimensions, etc., and for cyberforensic reasoning as one of the use-cases of interest. Thus, GIPSY is a support testbed for HOIL-based languages some of which enable such reasoning, as in formal cyberforensic case analysis with event reconstruction. In this paper we discuss the GIPSY architecture, its evaluation engine and example use-cases.
△ Less
Submitted 21 June, 2009;
originally announced June 2009.
-
Towards Automated Deduction in Blackmail Case Analysis with Forensic Lucid
Authors:
Serguei A. Mokhov,
Joey Paquet,
Mourad Debbabi
Abstract:
This work-in-progress focuses on the refinement of application of the intensional logic to cyberforensic analysis and its benefits are compared with the finite-state automata approach. This work extends the use of the scientific intensional programming paradigm onto modeling and implementation of a cyberforensics investigation process with the backtrace of event reconstruction, modeling the evid…
▽ More
This work-in-progress focuses on the refinement of application of the intensional logic to cyberforensic analysis and its benefits are compared with the finite-state automata approach. This work extends the use of the scientific intensional programming paradigm onto modeling and implementation of a cyberforensics investigation process with the backtrace of event reconstruction, modeling the evidence as multidimensional hierarchical contexts, and proving or disproving the claims with it in the intensional manner of evaluation. This is a practical, context-aware improvement over the finite state automata (FSA) approach we have seen in the related works. As a base implementation language model we use in this approach is a new dialect of the Lucid programming language, that we call Forensic Lucid and in this paper we focus on defining hierarchical contexts based on the intensional logic for the evaluation of cyberforensic expressions.
△ Less
Submitted 29 May, 2009;
originally announced June 2009.
-
Formally Specifying and Proving Operational Aspects of Forensic Lucid in Isabelle
Authors:
Serguei A. Mokhov,
Joey Paquet
Abstract:
A Forensic Lucid intensional programming language has been proposed for intensional cyberforensic analysis. In large part, the language is based on various predecessor and codecessor Lucid dialects bound by the higher-order intensional logic (HOIL) that is behind them. This work formally specifies the operational aspects of the Forensic Lucid language and compiles a theory of its constructs usin…
▽ More
A Forensic Lucid intensional programming language has been proposed for intensional cyberforensic analysis. In large part, the language is based on various predecessor and codecessor Lucid dialects bound by the higher-order intensional logic (HOIL) that is behind them. This work formally specifies the operational aspects of the Forensic Lucid language and compiles a theory of its constructs using Isabelle, a proof assistant system.
△ Less
Submitted 23 April, 2009;
originally announced April 2009.
