A Modular Type Reconstruction Algorithm

2018 ◽  
Vol 19 (4) ◽  
pp. 1-43 ◽  
Author(s):  
Florian Rabe
Keyword(s):  
Reconstruction Algorithm ◽  
Type Reconstruction

scholarly journals SART-Type Image Reconstruction from Overlapped Projections

2011 ◽  
Vol 2011 ◽  
pp. 1-7
Author(s):  
Hengyong Yu ◽  
Changguo Ji ◽  
Ge Wang
Keyword(s):  
Image Reconstruction ◽  
Reconstruction Algorithm ◽  
Reconstruction Technique ◽  
Algebraic Reconstruction Technique ◽  
Multiple Sources ◽  
X Ray ◽  
Type Reconstruction ◽  
Soft Threshold ◽  
Simultaneous Algebraic Reconstruction Technique ◽  
Data Acquisition Process

To maximize the time-integrated X-ray flux from multiple X-ray sources and shorten the data acquisition process, a promising way is to allow overlapped projections from multiple sources being simultaneously on without involving the source multiplexing technology. The most challenging task in this configuration is to perform image reconstruction effectively and efficiently from overlapped projections. Inspired by the single-source simultaneous algebraic reconstruction technique (SART), we hereby develop a multisource SART-type reconstruction algorithm regularized by a sparsity-oriented constraint in the soft-threshold filtering framework to reconstruct images from overlapped projections. Our numerical simulation results verify the correctness of the proposed algorithm and demonstrate the advantage of image reconstruction from overlapped projections.

scholarly journals Higher-Ranked Annotation Polymorphic Dependency Analysis

2020 ◽  
pp. 656-683 ◽  
Author(s):  
Fabian Thorand ◽  
Jurriaan Hage
Keyword(s):  
Static Analysis ◽  
Type System ◽  
Reconstruction Algorithm ◽  
Context Sensitivity ◽  
Functional Languages ◽  
Dependency Analysis ◽  
One Step ◽  
Type Reconstruction ◽  
Generic Analysis

AbstractThe precision of a static analysis can be improved by increasing the context-sensitivity of the analysis. In a type-based formulation of static analysis for functional languages this can be achieved by, e.g., introducing let-polyvariance or subtyping. In this paper we go one step further by defining a higher-ranked polyvariant type system so that even properties of lambda-bound identifiers can be generalized over. We do this for dependency analysis, a generic analysis that can be instantiated to a range of different analyses that in this way all can profit.We prove that our analysis is sound with respect to a call-by-name semantics and that it satisfies a so-called noninterference property. We provide a type reconstruction algorithm that we have proven to be terminating, and sound and complete with respect to its declarative specification. Our principled description can serve as a blueprint for making other analyses higher-ranked.

scholarly journals An insider's look at LF type reconstruction: everything you (n)ever wanted to know

2012 ◽  
Vol 23 (1) ◽  
pp. 1-37 ◽  
Author(s):  
BRIGITTE PIENTKA
Keyword(s):  
Reconstruction Algorithm ◽  
Logical Framework ◽  
Reconstruction Process ◽  
Correctness Proofs ◽  
Free Variables ◽  
Type Reconstruction ◽  
Typed Languages ◽  
Modal Types

AbstractAlthough type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-pass type reconstruction for objects in the logical framework LF, describe formally the type reconstruction process using the framework of contextual modal types, and prove correctness of type reconstruction. Since type reconstruction will find most general types and may leave free variables, we in addition describe abstraction which will return a closed object where all free variables are bound at the outside. We also implemented our algorithms as part of the Beluga language, and the performance of our type reconstruction algorithm is comparable to type reconstruction in existing systems such as the logical framework Twelf.

Lilac: a functional programming language based on linear logic

1994 ◽  
Vol 4 (4) ◽  
pp. 395-433 ◽  
Author(s):  
Ian Mackie
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Linear Logic ◽  
Reconstruction Algorithm ◽  
Linear Term ◽  
Control Information ◽  
Functional Programming Language ◽  
Type Reconstruction ◽  
And Control ◽  
Intuitionistic Linear Logic

AbstractWe take Abramsky's term assignment for Intuitionistic Linear Logic (the linear term calculus) as the basis of a functional programming language. This is a language where the programmer must embed explicitly the resource and control information of an algorithm. We give a type reconstruction algorithm for our language in the style of Milner's W algorithm, together with a description of the implementation and examples of use.

Nondestructive Inspection of Thin, Low-Z Samples using Multiplexed Compton Scatter Tomography

1997 ◽  
Vol 503 ◽  
Author(s):  
B. L. Evans ◽  
J. B. Martin ◽  
L. W. Burggraf
Keyword(s):  
Signal To Noise Ratio ◽  
Reconstruction Algorithm ◽  
Filtered Backprojection ◽  
Line Broadening ◽  
Compton Scatter ◽  
X Ray ◽  
Tomography System ◽  
Transmission Computed Tomography ◽  
High Purity Germanium ◽  
Scattered Energy

ABSTRACTThe viability of a Compton scattering tomography system for nondestructively inspecting thin, low Z samples for corrosion is examined. This technique differs from conventional x-ray backscatter NDI because it does not rely on narrow collimation of source and detectors to examine small volumes in the sample. Instead, photons of a single energy are backscattered from the sample and their scattered energy spectra are measured at multiple detector locations, and these spectra are then used to reconstruct an image of the object. This multiplexed Compton scatter tomography technique interrogates multiple volume elements simultaneously. Thin samples less than 1 cm thick and made of low Z materials are best imaged with gamma rays at or below 100 keV energy. At this energy, Compton line broadening becomes an important resolution limitation. An analytical model has been developed to simulate the signals collected in a demonstration system consisting of an array of planar high-purity germanium detectors. A technique for deconvolving the effects of Compton broadening and detector energy resolution from signals with additive noise is also presented. A filtered backprojection image reconstruction algorithm with similarities to that used in conventional transmission computed tomography is developed. A simulation of a 360–degree inspection gives distortion-free results. In a simulation of a single-sided inspection, a 5 mm × 5 mm corrosion flaw with 50% density is readily identified in 1-cm thick aluminum phantom when the signal to noise ratio in the data exceeds 28.

Sign in / Sign up

Export Citation Format

Share Document