ML

swMATH1218MaRDI QIDQ13958FDOQ13958

Author name not available (Why is that?)

Described by source

• A theory of type polymorphism in programming
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Deductive and inductive synthesis of equational programs
• A Scalable Inclusion Constraint Solver Using Unification
• Game theoretic analysis of call-by-value computation
• A language for generic programming in the large
• Extended Static Checking by Calculation Using the Pointfree Transform
• Region-based memory management
• Genericity and the \(\pi\)-calculus
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Unifying sets and programs via dependent types
• Introduction to Type Theory
• The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
• Formal reliability analysis of combinational circuits using theorem proving
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• A rewriting logic approach to operational semantics
• Improving type error messages for generic Java
• The correctness of Newman's typability algorithm and some of its extensions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Typed generic traversal with term rewriting strategies
• Combining Decision Procedures by (Model-)Equality Propagation
• Parametric higher-order abstract syntax for mechanized semantics
• On the existence of free models in abstract algebraic institutions
• XML with data values: Typechecking revisited.
• Higher-order rewrite systems and their confluence
• MetaML and multi-stage programming with explicit annotations
• A framework for the verification of certifying computations
• Mechanised support for sound refinement tactics
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• Monotonicity inference for higher-order formulas
• Computability in higher types, P\(\omega\) and the completeness of type assignment
• Forum: A multiple-conclusion specification logic
• The locally nameless representation
• Recasting ML\(^{\text F}\)
• A characterization of F-complete type assignments
• Completeness of type assignment in continuous lambda models
• Polymorphic type inference and containment
• Exploring structural symmetry automatically in symbolic trajectory evaluation
• An algebraic semantics approach to the effective resolution of type equations
• Implicit propagation in structural operational semantics
• An analysis of Böhm's theorem
• Executable structural operational semantics in Maude
• Extending the type checker of Standard ML by polymorphic recursion
• Optimizing proof search in model elimination
• A linear logical framework
• Implementing compositional analysis using intersection types with expansion variables
• The representational adequacy of Hybrid
• The sequentially realizable functionals
• Proof-producing synthesis of ML from higher-order logic
• Automatic verification of reduction techniques in higher order logic
• An inductive approach to strand spaces
• Database query languages and functional logic programming
• Domain-free \(\lambda\mu\)-calculus
• A tactic calculus. --- Abridged version
• The completeness theorem for typing lambda-terms
• A Rewriting Logic Approach to Type Inference
• A Polymorphic Type System for the Lambda-Calculus with Constructors
• Shallow confluence of conditional term rewriting systems
• Typing termination in a higher-order concurrent imperative language
• Data compression for proof replay
• A reflective functional language for hardware design and theorem proving
• Ordinal arithmetic: Algorithms and mechanization
• From reduction-based to reduction-free normalization
• A theory of bisimulation for a fragment of concurrent ML with local names
• Formal verification of tail distribution bounds in the HOL theorem prover
• The complexity of higher-order queries
• Bio-PEPAd: a non-Markovian extension of Bio-PEPA
• Secure mechanical verification of mutually recursive procedures
• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving
• Title not available (Why is that?)
• Call-by-value Solvability
• An approach for lifetime reliability analysis using theorem proving
• Full abstraction for Reduced ML
• Semantic types and approximation for Featherweight Java
• An approach to completing variable names for implicitly typed functional languages
• On graph rewriting, reduction, and evaluation in the presence of cycles
• Essential concepts of algebraic specification and program development
• Formal Analysis of Optical Waveguides in HOL
• Term Rewriting and All That
• Semantic essence of AsmL
• Principal type scheme and unification for intersection type discipline
• Towards Knowledge Management for HOL Light
• Complete restrictions of the intersection type discipline
• Intersection type assignment systems
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Computer Aided Verification
• Contract-based verification of MATLAB-style matrix programs
• A decision procedure for linear ``big O equations
• Computational interpretations of linear logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• PCF extended with real numbers
• A Brief Overview of HOL4
• The higher-order prover \textsc{Leo}-II
• Semi-intelligible Isar proofs from machine-generated proofs
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• The Orc Programming Language
• An observationally complete program logic for imperative higher-order functions
• Game-theoretic analysis of call-by-value computation

This page was built for software: ML