Hoare type theory, polymorphism and separation

2008 ◽  
Vol 18 (5-6) ◽  
pp. 865-911 ◽  
Author(s):  
ALEKSANDAR NANEVSKI ◽  
GREG MORRISETT ◽  
LARS BIRKEDAL
Keyword(s):  
Type Theory ◽  
Higher Order ◽  
Separation Logic ◽  
Functional Language ◽  
Individual Program ◽  
Small Footprint ◽  
Program Components ◽  
Pointer Aliasing ◽  
Higher Order Functions ◽  
Order State

AbstractWe consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and nontermination. We propose Hoare type theory (HTT), which incorporates Hoare-style specifications into types, making it possible to statically track and enforce correct use of side effects.The main feature of HTT is the Hoare type {P}x:A{Q} specifying computations with preconditionPand postconditionQthat return a result of typeA. Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism.We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the “small footprint” manner, as advocated by separation logic, whereby specifications tightly describe the state required by the computation.We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.

scholarly journals Higher order interpretation for higher order complexity

10.29007/1tkw ◽  
2018 ◽  
Author(s):  
Emmanuel Hainry ◽  
Romain Péchoux
Keyword(s):  
Complexity Analysis ◽  
Higher Order ◽  
Functional Language ◽  
Higher Order Functions

We design an interpretation-based theory of higher-order functions that is well-suited for the complexity analysis of a standard higher- order functional language a` la ml. We manage to express the interpretation of a given program in terms of a least fixpoint and we show that when restricted to functions bounded by higher-order polynomials, they characterize exactly classes of tractable functions known as Basic Feasible Functions at any order.

scholarly journals Connecting Higher-Order Separation Logic to a First-Order Outside World

2020 ◽  
pp. 428-455 ◽  
Author(s):  
William Mansky ◽  
Wolf Honoré ◽  
Andrew W. Appel
Keyword(s):  
Program Verification ◽  
Higher Order ◽  
Separation Logic ◽  
C Programs ◽  
First Order ◽  
System Calls ◽  
Correctness Of Programs ◽  
Verified Software ◽  
Order State ◽  
Order Separation

AbstractSeparation logic is a useful tool for proving the correctness of programs that manipulate memory, especially when the model of memory includes higher-order state: Step-indexing, predicates in the heap, and higher-order ghost state have been used to reason about function pointers, data structure invariants, and complex concurrency patterns. On the other hand, the behavior of system features (e.g., operating systems) and the external world (e.g., communication between components) is usually specified using first-order formalisms. In principle, the soundness theorem of a separation logic is its interface with first-order theorems, but the soundness theorem may implicitly make assumptions about how other components are specified, limiting its use. In this paper, we show how to extend the higher-order separation logic of the Verified Software Toolchain to interface with a first-order verified operating system, in this case CertiKOS, that mediates its interaction with the outside world. The resulting system allows us to prove the correctness of C programs in separation logic based on the semantics of system calls implemented in CertiKOS. It also demonstrates that the combination of interaction trees + CompCert memories serves well as a lingua franca to interface and compose two quite different styles of program verification.

A polymorphic library for constructive solid geometry

1995 ◽  
Vol 5 (3) ◽  
pp. 415-442
Author(s):  
J. R. Davy ◽  
P. M. Dew
Keyword(s):  
Higher Order ◽  
Divide And Conquer ◽  
Functional Language ◽  
Constructive Solid Geometry ◽  
Solid Modelling ◽  
General Applicability ◽  
Solid Geometry ◽  
Recurrent Patterns ◽  
Higher Order Functions

AbstractSolid modelling using constructive solid geometry (CSG) includes many examples of stylised divide-and-conquer algorithms. We identify the sources of these recurrent patterns and describe a Geometric Evaluation Library (GEL) which captures them as higher-order functions. This library then becomes the basis of developing CSG applications quickly and concisely. GEL is currently implemented as a set of separately compiled modules in the pure functional language Hope+. We evaluate our work in terms of performance and general applicability. We also assess the benefits of the functional paradigm in this domain and the merits of programming with a set of higher-order functions.

scholarly journals ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Dan Frumin ◽  
Robbert Krebbers ◽  
Lars Birkedal
Keyword(s):  
Symbolic Execution ◽  
Higher Order ◽  
Separation Logic ◽  
Structural Rules ◽  
Fine Grained ◽  
The Core ◽  
Proof Rules ◽  
Interactive Proofs ◽  
Relational Logic ◽  
Order State

We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines a program $e'$ at type $\tau$. ReLoC provides type-directed structural rules and symbolic execution rules in separation-logic style for manipulating the judgment, whereas in prior work on refinements for languages with higher-order state and concurrency, such proofs were carried out by unfolding the judgment into its definition in the model. ReLoC's abstract proof rules make it simpler to carry out refinement proofs, and enable us to generalize the notion of logically atomic specifications to the relational case, which we call logically atomic relational specifications. We build ReLoC on top of the Iris framework for separation logic in Coq, allowing us to leverage features of Iris to prove soundness of ReLoC, and to carry out refinement proofs in ReLoC. We implement tactics for interactive proofs in ReLoC, allowing us to mechanize several case studies in Coq, and thereby demonstrate the practicality of ReLoC. ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a new Coq mechanization, and support for Iris's prophecy variables. The latter allows us to carry out refinement proofs that involve reasoning about the program's future. We also expand ReLoC's notion of logically atomic relational specifications with a new flavor based on the HOCAP pattern by Svendsen et al.

PROLOG'S CONTROL CONSTRUCTS IN A FUNCTIONAL SETTING — AXIOMS AND IMPLEMENTATION

2001 ◽  
Vol 12 (02) ◽  
pp. 125-170 ◽  
Author(s):  
RALF HINZE
Keyword(s):  
Canonical Form ◽  
Higher Order ◽  
Exception Handling ◽  
Functional Language ◽  
Iso Standard ◽  
Error Handling ◽  
Definition Of ◽  
Functional Setting ◽  
Higher Order Functions

The purpose of this article is twofold. First, we show that Prolog's control constructs can be smoothly integrated into a functional language like Haskell. The resulting 'language', termed embedded Prolog, incorporates many of the features prescribed by the Prolog ISO standard: control constructs including the cut, all solution collecting functions, and error handling facilities. Embedded Prolog lacks some concepts such as logical variables but it inherits all of Haskell's strengths, eg static polymorphic typing, higher order functions etc. Technically, the integration is achieved using monads and monad transformers. One of the main innovations is the definition of a backtracking monad transformer, which allows us to combine backtracking with exception handling and interaction. Second, we work towards an axiomatization of the operations, through which the computational features are accessed. Equations are used to lay down the meaning of the various operations and their interrelations enabling the programmer to reason about programs in a simple calculational style. The axiomatization is applied to show that each finite computation has a simple canonical form.

Computational Models for Multilayered Composite Shells with Application to Tires

1996 ◽  
Vol 24 (1) ◽  
pp. 11-38 ◽  
Author(s):  
G. M. Kulikov
Keyword(s):  
Type Theory ◽  
Computational Models ◽  
Geometrical Nonlinearity ◽  
Higher Order ◽  
Stress Strain ◽  
Strain Fields ◽  
First Order ◽  
Timoshenko Type ◽  
Joint Influence ◽  
Discrete Layer

Abstract This paper focuses on four tire computational models based on two-dimensional shear deformation theories, namely, the first-order Timoshenko-type theory, the higher-order Timoshenko-type theory, the first-order discrete-layer theory, and the higher-order discrete-layer theory. The joint influence of anisotropy, geometrical nonlinearity, and laminated material response on the tire stress-strain fields is examined. The comparative analysis of stresses and strains of the cord-rubber tire on the basis of these four shell computational models is given. Results show that neglecting the effect of anisotropy leads to an incorrect description of the stress-strain fields even in bias-ply tires.

Higher Order Theory

2018 ◽  
Author(s):  
J. Christopher Maloney
Keyword(s):  
Phenomenal Character ◽  
Order Theory ◽  
Higher Order ◽  
Cognitive State ◽  
Unconscious Perception ◽  
Higher Order Theory ◽  
Order State

Rosenthal's rendition of representationalism denies intentionalism. His higher order theory instead asserts that a perceptual state's phenomenal character is set by that state's being related to, because represented by, another, but higher order, cognitive state. The theory arises from the doubtful supposition of unconscious perception and mistakenly construes intrinsic phenomenal character extrinsically, as one state's serving as the content of another. Yet it remains mysterious how and why a higher order state might be so potent as to determine phenomenal character at all. Better to resist higher order theory’s embrace of dubious unconscious perceptual states and account for states so-called simply in terms of humdrum mnemonic malfeasance. Moreover, since the suspect theory allows higher order misrepresentation, it implies sufferance of impossible phenomenal character. Equally problematic, representationalism pitched at the higher order entails the existence of bogus phenomenal character when upstairs states represent downstairs nonperceptual states.

scholarly journals Distributed causal memory: modular specification and verification in higher-order distributed separation logic

2021 ◽  
Vol 5 (POPL) ◽  
pp. 1-29
Author(s):  
Léon Gondelman ◽  
Simon Oddershede Gregersen ◽  
Abel Nieto ◽  
Amin Timany ◽  
Lars Birkedal
Keyword(s):  
Higher Order ◽  
Separation Logic ◽  
Specification And Verification

scholarly journals Voigt Transform and Umbral Image

2020 ◽  
Vol 25 (3) ◽  
pp. 49
Author(s):  
Silvia Licciardi ◽  
Rosa Maria Pidatella ◽  
Marcello Artioli ◽  
Giuseppe Dattoli
Keyword(s):  
Spectroscopic Studies ◽  
Higher Order ◽  
Point Of View ◽  
The Other ◽  
Pivotal Role ◽  
Umbral Calculus ◽  
Laguerre Functions ◽  
Hermite And Laguerre Functions ◽  
Higher Order Functions ◽  
Voigt Function

In this paper, we show that the use of methods of an operational nature, such as umbral calculus, allows achieving a double target: on one side, the study of the Voigt function, which plays a pivotal role in spectroscopic studies and in other applications, according to a new point of view, and on the other, the introduction of a Voigt transform and its possible use. Furthermore, by the same method, we point out that the Hermite and Laguerre functions, extension of the corresponding polynomials to negative and/or real indices, can be expressed through a definition in a straightforward and unified fashion. It is illustrated how the techniques that we are going to suggest provide an easy derivation of the relevant properties along with generalizations to higher order functions.

Sign in / Sign up

Export Citation Format

Share Document