Synthesis of ML programs in the system Coq
type: Item
instance of: scholarly article
title: Synthesis of ML programs in the system Coq
zbMATH Open document ID: 0804.68132
DOI: 10.1016/S0747-7171(06)80007-6
author: Christine Paulin-Mohring
author: Benjamin Werner
published in: Journal of Symbolic Computation
publication date: 1995-01-12T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N15
zbMATH DE Number: 566068
zbMATH Keywords: program synthesis
zbMATH Keywords: calculus of constructions
zbMATH Keywords: optimization
zbMATH Keywords: Coq
zbMATH Keywords: proof development
zbMATH Keywords: functional program
zbMATH Keywords: ML
zbMATH Keywords: primitive recursive functionals
zbMATH Keywords: termination
zbMATH Keywords: fixpoint
describes a project that uses: Coq
describes a project that uses: LCF
describes a project that uses: ML
describes a project that uses: Nuprl
MaRDI profile type: Publication
cites work: Q3490989
cites work: Q3703866
cites work: Q3030827
cites work: Q5753923
cites work: Comparing integrated and external logics of functional programs
cites work: Q3994895
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q3997016
cites work: Q3477935
cites work: Q3997125
cites work: Q3883562
cites work: Q3688389
cites work: Terminating general recursion
cites work: Q3999860
cites work: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
cites work: Q4281483
cites work: Proving termination of normalization functions for conditional expressions
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
full work available at URL: s0747-7171(06)80007-6
OpenAlex ID: W2135625856
description: scientific article; zbMATH DE number 566068