OCaml

swMATH6363MaRDI QIDQ18489FDOQ18489

Author name not available (Why is that?)

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

• Turning Inductive into Equational Specifications
• Explicit effect subtyping
• Title not available (Why is that?)
• A functional language to implement the divide-and-conquer Delaunay triangulation algorithm
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• Tree Components Programming: An Application to XML
• Title not available (Why is that?)
• Algorithms and proofs inheritance in the FOC language
• Optimizing nested loops using local CPS conversion
• Stream fusion, to completeness
• A proof dedicated meta-language
• A simple library implementation of binary sessions
• Declarative foreign function binding through generic programming
• Program verification by coinduction
• Semantics of typed lambda-calculus with constructors
• OCaml scientific computing. Functional programming in data science and artificial intelligence
• More on balanced diets
• A formal semantics for protocol narrations
• FFT program generation for ring LWE-based cryptography
• Experience of improving the BLAST static verification tool
• Proofs of a set of hybrid let-polymorphic type inference algorithms
• Compact bit encoding schemes for simply-typed lambda-terms
• Implementing and reasoning about hash-consed data structures in Coq
• The First-Order Nominal Link
• Set-theoretic types for polymorphic variants
• On a monadic semantics for freshness
• Path resolution for nested recursive modules
• Generating C. System description
• Safe zero-cost coercions for Haskell
• Purely functional lazy non-deterministic programming
• Proof pearl: constructive extraction of cycle finding algorithms
• Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
• Authenticated data structures, generically
• Tactics for Reasoning Modulo AC in Coq
• Title not available (Why is that?)
• MetaOCaml server pages: web publishing as staged computation
• Implementing hash-consed structures in Coq
• Herod and Pilate: two tableau provers for basic hybrid logic
• Title not available (Why is that?)
• Practical SMT-based type error localization
• A certifying square root and division elimination
• Title not available (Why is that?)
• Time warps, from algebra to algorithms
• A unifying approach to goal-directed evaluation
• Purely functional lazy nondeterministic programming
• A certified constraint solver over finite domains
• Title not available (Why is that?)
• Removing algebraic data types from constrained Horn clauses using difference predicates
• An efficient approach to nominal equalities in hybrid logic tableaux
• Programs using syntax with first-class binders
• Context-free session type inference
• Single Assignment C: efficient support for high-level array operations in a functional setting
• Virtual-machine-based heterogeneous checkpointing
• Improving parity games in practice
• From Sets to Bits in Coq
• OCaml + XDuce
• Counterexample-guided partial bounding for recursive function synthesis
• Building reliable, high-performance networks with the Nuprl proof development system
• Tilings as a programming exercise.
• Termination Proofs for Recursive Functions in FoCaLiZe
• Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9--15, 2000. Advanced lectures
• Anti-patterns for rule-based languages
• Adapting functional programs to higher order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• A Coq library for internal verification of running-times
• Programming Languages and Systems
• Verified characteristic formulae for CakeML
• Matching and alpha-equivalence check for nominal terms
• Title not available (Why is that?)
• A constructive theory of continuous domains suitable for implementation
• Formal compiler construction in a logical framework
• Title not available (Why is that?)
• NESTED ALGORITHMIC SKELETONS FROM HIGHER ORDER FUNCTIONS
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Certified roundoff error bounds using semidefinite programming
• Lightweight static capabilities
• Tool-assisted specification and verification of typed low-level languages
• Extending Coq with Imperative Features and Its Application to SAT Verification
• A verified proof checker for higher-order logic
• F-ing modules
• Customizing an XML-Haskell data binding with type isomorphism inference in generic Haskell
• Implementing nominal unification
• A type system for bounded space and functional in-place update
• Dependent types from counterexamples
• Mathematical knowledge management in Foc
• Formalization of Wu's simple method in Coq
• An operational semantics for object-oriented concepts based on the class hierarchy
• Producing all ideals of a forest, functionally
• Implementing real numbers with RZ
• The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq
• Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming
• An Interpretation of Isabelle/HOL in HOL Light
• Certifying properties of an efficient functional program for computing Gröbner bases
• Automatic Termination Verification for Higher-Order Functional Programs
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• Dependency-style generic Haskell
• Programming languages and systems. 17th European symposium on programming, ESOP 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings

This page was built for software: OCaml