Adapting functional programs to higher order logic
From MaRDI portal
Publication:1029815
DOI10.1007/s10990-008-9038-0zbMath1175.68103OpenAlexW2092268590MaRDI QIDQ1029815
Publication date: 13 July 2009
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10990-008-9038-0
higher-order logicterminationwell-foundednessrecursive definitionregular expression pattern matching
Symbolic computation and algebraic computation (68W30) Functional programming and lambda calculus (68N18)
Related Items (8)
POSIX lexing with derivatives of regular expressions ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl) ⋮ POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions ⋮ Proof-producing translation of higher-order logic into pure and stateful ML
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- From regular expressions to deterministic automata
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Proving and applying program transformations expressed with second-order patterns
- IMPS: An interactive mathematical proof system
- Termination of nested and mutually recursive algorithms
- Partial functions in ACL2
- Isabelle/HOL. A proof assistant for higher-order logic
- Edinburgh LCF. A mechanized logic of computation
- Dependent types for program termination verification
- On equivalents of well-foundedness. An experiment in MIZAR
- Proof producing synthesis of arithmetic and cryptographic hardware
- A predicative analysis of structural recursion
- Regular expression pattern matching for XML
- Applications of Polytypism in Theorem Proving
- HOLCF = HOL + LCF
- A Thread of HOL Development
- Verification of non-functional programs using interpretations in type theory
- Building reliable, high-performance networks with the Nuprl proof development system
- Proof-directed debugging
- Implicit parameters
- The size-change principle for program termination
- Cayenne—a language with dependent types
- The under-appreciated unfold
- Efficient execution in an automated reasoning environment
- Automata, Languages and Programming
- Programming Techniques: Regular expression search algorithm
- Derivatives of Regular Expressions
- Enumerating the strings of regular languages
- Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
- Termination Analysis with Calling Context Graphs
- A formulation of the simple theory of types
This page was built for publication: Adapting functional programs to higher order logic
