Browsing by Author "Wang, Yuting"
Now showing 1 - 2 of 2
Results Per Page
Sort Options
Item Finite Size Scaling Around One Dimensional Topological Quantum Phase Transitions(2020-05) Wang, YutingThe critical point of a topological phase transition is described by a conformal field theory. We first investigate the finite-size scaling away from criticality of the ground state energy and find a scaling function, which discriminates between phases with different topological indexes. This function appears to be universal for all five Altland-Zirnbauer symmetry classes with non-trivial topology in one spatial dimension. We obtain an analytic form of the scaling function and compare it with numerical results. Then we verify the universality of the scaling function for the topological transition between dimerized and Haldane phases in bilinear-biquadratic spin-1 chain. To this end we perform high-accuracy variational matrix product state simulations. We show that the scaling function, expressed in terms of $L/\xi$, where $L$ is the chain length and $\xi$ is the correlation length, coincides with that of three species of non-interacting massive Majorana fermions. The latter is known to be a proper description of the conformal critical theory with central charge $c=3/2$. We have shown that it still holds away from the conformal point, including the finite size corrections. Finally we consider scaling of the entanglement entropy across a topological quantum phase transition for the Kitaev chain model. The change of the topology manifests itself in a sub-leading term, which scales as $L^{-1/\alpha}$ with the size of the subsystem $L$, here $\alpha$ is the R\'{e}nyi index. This term reveals the scaling function $h_\alpha(L/\xi)$, where $\xi$ is the correlation length, which is sensitive to the topological index. The scaling function $h_\alpha(L/\xi)$ is independent of model parameters, suggesting some degree of its universality.Item A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs(2016-12) Wang, YutingThis thesis concerns the verified compilation of functional programming languages. Functional programming languages, or functional languages for short, provide a high degree of abstraction in programming and their mathematical foundation makes programs written in them easy to analyze and to be proved correct. Because of these features, functional languages are playing an increasingly important role in modern software development. However, there is a gap that must be closed before we can derive the full benefits of verifying programs written in functional languages. Programs are usually verified with regard to the computational models underlying the functional languages, while the execution of programs proceeds only after they are transformed by compilers into a form that is executable on real hardware. To get programs verified end-to-end, the compilers must also be proved correct. Significant strides have been taken in recent years towards the goal of verifying compilers. However, much of the attention in this context has been on imperative programming languages. The verification of compilers for functional languages poses some additional challenges. A defining characteristic of such languages is that they treat functions as first-class objects. In describing the compilation of programs written in functional languages and in reasoning about this compilation, it is therefore necessary to treat functions as data objects. In particular, we need to provide a logically correct treatment of the relationship between the arguments of a function and their use within its body, i.e., the binding structure of the function. Most existing proof systems for formal verification provide only very primitive support for reasoning about binding structure. As a result, significant effort needs to be expended to reason about substitutions and other aspects of binding structure and this complicates and sometimes overwhelms the task of verifying compilers for functional languages. We argue that the implementation and verification of compilers for functional languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying idea of HOAS is to use a meta-language that provides a built-in and logical treatment of binding related notions. By embedding the meta-language within a larger programming or reasoning framework, it is possible to absorb the treatment of binding structure in the object language into the meta-theory of the system, thereby greatly simplifying the overall implementation and reasoning processes. We develop the above argument in this thesis. In particular, we present and demonstrate the effectiveness of an approach to the verified implementation of compiler transformations for functional programs that exploits HOAS. In this approach, transformations on functional programs are first articulated in the form of rule-based relational specifications. These specifications are rendered into programs in lambda Prolog, a language that is well-suited to encoding rule-based relational specifications and that supports an HOAS-style treatment of formal objects such as programs. Programs in lambda Prolog serve both as specifications and as executable code. One consequence of this is that the encodings of compiler transformations serve directly as their implementations. Another consequence is that they can be input to the theorem proving system Abella that provides rich capabilities for reasoning about such specifications and thereby for proving their correctness as implementations. The Abella system also supports the use of the HOAS approach. Thus, the lambda Prolog language and the Abella system together constitute a framework that can be used to test out the benefits of the HOAS approach in verified compilation. We use them to implement and verify a compiler for a representative functional programming language that embodies the transformations that form the core of many compilers for such languages. In both the programming and the reasoning phases, we show how the use of the HOAS approach significantly simplifies the representation, manipulation, analysis and reasoning of binding structure. Carrying out the above exercise revealed some missing capabilities in the Abella system. At the outset, it was possible to reason about only a subset of lambda Prolog programs using the system. Some compiler transformations required the use of features not available in this subset. Another limitation was that it did not support the ability to reason about polymorphic specifications, thereby leading to a loss of modularity in programs and in reasoning. We have addressed these issues as well in this thesis. In particular, we have developed the theoretical underpinnings for introducing polymorphism into Abella and for treating the full range of lambda Prolog specifications. These ideas have also been implemented to yield a new version of Abella with the additional capabilities.