OCaml

swMATH6363MaRDI QIDQ18489

No author found.

Related Items (only showing first 100 items - show all)

Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9--15, 2000. Advanced lectures ⋮ OCaml scientific computing. Functional programming in data science and artificial intelligence ⋮ FFT program generation for ring LWE-based cryptography ⋮ Counterexample-guided partial bounding for recursive function synthesis ⋮ An efficient approach to nominal equalities in hybrid logic tableaux ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Why does Astrée scale up? ⋮ Compilation of extended recursion in call-by-value functional languages ⋮ Embedding an interpreted language using higher-order functions and types ⋮ Formal compiler construction in a logical framework ⋮ Unnamed Item ⋮ Tool-assisted specification and verification of typed low-level languages ⋮ Generating C. System description ⋮ Customizing an XML-Haskell data binding with type isomorphism inference in generic Haskell ⋮ An expressive language of signatures ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ An efficient abstract machine for safe ambients ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Path resolution for nested recursive modules ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Delimited control in OCaml, abstractly and concretely ⋮ Programming language concepts. With a chapter by Niels Hallenberg ⋮ Time warps, from algebra to algorithms ⋮ Designing and proving correct a convex hull algorithm with hypermaps in Coq ⋮ Multi-task implementation of multi-periodic synchronous programs ⋮ Inheritance in the join calculus. ⋮ Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves ⋮ Greedily computing associative aggregations on sliding windows ⋮ Programming with algebraic effects and handlers ⋮ The foundation of self-developing blob machines for spatial computing ⋮ Lem ⋮ Fiat ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Amortized complexity verified ⋮ A formal semantics for protocol narrations ⋮ A paraconsistent logic programming approach for querying inconsistent databases ⋮ A verified proof checker for higher-order logic ⋮ NESTED ALGORITHMIC SKELETONS FROM HIGHER ORDER FUNCTIONS ⋮ Coalgebras for Binary Methods: Properties of Bisimulations and Invariants ⋮ Unnamed Item ⋮ 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 ⋮ Experience of improving the BLAST static verification tool ⋮ Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code ⋮ A type system for reflective program generators ⋮ Unnamed Item ⋮ Proofs of a set of hybrid let-polymorphic type inference algorithms ⋮ Anti-patterns for rule-based languages ⋮ Hybrid automata, reachability, and systems biology ⋮ Browndye: A software package for Brownian dynamics ⋮ Incremental reasoning with lazy behavioral subtyping for multiple inheritance ⋮ Reachability analysis over term rewriting systems ⋮ Matching and alpha-equivalence check for nominal terms ⋮ MetaOCaml server pages: web publishing as staged computation ⋮ Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem ⋮ Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac} ⋮ Proof pearl: constructive extraction of cycle finding algorithms ⋮ From Sets to Bits in Coq ⋮ A Coq Library for Internal Verification of Running-Times ⋮ Declarative Foreign Function Binding Through Generic Programming ⋮ Termination criteria for tree automata completion ⋮ Implementing hybrid semantics: from functional to imperative ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Improving parity games in practice ⋮ Models of computation. An introduction to computability theory ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ A certifying square root and division elimination ⋮ Certifying properties of an efficient functional program for computing Gröbner bases ⋮ Termination Proofs for Recursive Functions in FoCaLiZe ⋮ Safe zero-cost coercions for Haskell ⋮ Algorithms for compact letter displays: comparison and evaluation ⋮ A constructive theory of continuous domains suitable for implementation ⋮ Dependent types and multi-monadic effects in F* ⋮ Chapar: certified causally consistent distributed key-value stores ⋮ Adapting functional programs to higher order logic ⋮ Unnamed Item ⋮ Explicit effect subtyping ⋮ Program verification by coinduction ⋮ A compact kernel for the calculus of inductive constructions ⋮ Functional specification and prototyping with oriented combinatorial maps ⋮ On a monadic semantics for freshness ⋮ Extracting a data flow analyser in constructive logic ⋮ Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls ⋮ AtomCaml ⋮ Semantic essence of AsmL ⋮ A functional language to implement the divide-and-conquer Delaunay triangulation algorithm ⋮ Smart test data generators via logic programming ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Inheritance-based subtyping ⋮ CC(X): Semantic Combination of Congruence Closure with Solvable Theories ⋮ Lightweight Static Capabilities ⋮ Implementing Nominal Unification ⋮ Tilings as a programming exercise. ⋮ Implementing and reasoning about hash-consed data structures in Coq ⋮ Algorithms and proofs inheritance in the FOC language ⋮ Optimizing nested loops using local CPS conversion ⋮ NLCertify: A Tool for Formal Nonlinear Optimization

This page was built for software: OCaml