CiteULike is a free online bibliography manager. Register
and you can start organising your references online.
Deliverables: A categorical approach to program development in type theory(1993)
|
Reviews
[Write a review of this article]
There are no reviews of this article
Find related articles from these CiteULike users Find related articles with these CiteULike tags AbstractThis thesis considers the problem of program correctness within a rich theory of dependent types, the Extended Calculus of Constructions (ECC). This system contains a powerful programming language of higher-order primitive recursion and higher-order intuitionistic logic. It is supported by Pollack's versatile LEGO implementation, which I use extensively to develop the mathematical constructions studied here. I systematically investigate Burstall's notion of deliverable, that is, a program...
BibTeX record RIS record2-categorical 2d 2-toposes 3d 3-lisp 3-manifold 4d abduction abductive abductive-inference absolute-motion abstracting abstraction abstract-machine abstract-neural-machine abstract-state-machines acceptability access accessibility accessible ace acoustic acquisition active-learning activeweb activity activity-based adaptability adaptation adaptive adaptive-object-models adaptivity adeles adelic adelic-space adjoint adjoint-functors adjunctions adl ads-universe aggregation aging ait aixi al algebra algebraic algebraic-domain algebraic-domains algebraic-dynamics algebraic-geometry algebraic-hierarchy algebraicity algebraic-lattice algebraic-manifold algebraic-model algebraic-process-theory algebraic-semiotics algebraic-structure algebraic-structures algebraic-theories algebraic-theory algebras algorithm algorithmic algorithmic-complexity algorithmic-information-content algorithmic-information-theory algorithmic-model-theory algorithmic-probability algorithmic-statistics algorithm-selection algorithm-theories algorithm-visualization alignment all-algebraic-categories all-algebraic-structures all-computational-structures allegory-theory all-logical-structures all-logical-theories all-mathematical-structures allocating allocation all-physical-structures all-possible-universes all-relational-structures all-small-categories alphabet alternation analogy analysis animation anisotropic anisotropy annotating annotation anthropic-principle anticipation anti-deterministic anti-intuitionistic anti-matroid anti-self-dual aop aose api applications approximable-concepts approximating approximation approximation-order ar arbitrage arbitrage-pricing-theory arbitrary-measure architecture archive argumantation argumentation argumentation-theory argumenting artificial-immune-system artificial-physics asm aspects aspectscode assembly asset-graph asset-lattice asset-network asset-space asset-tree assistance assistant association-graph association-rule association-rules assom astronomy asymmetric asymmetric-information asymmetry asymptotic asynchronous atomisticity atp attention attractor attractor-reconstruction attribute-exploration auction auctions auction-theory augmenting authoring automat automata automated-modeling automatic automatic-structures automating automation automorphism autonomic-computing autonomous-category auto-organizaiton autoresonant autowaves axiom axiomatic-domain-theory axiomatic-system axiomatisation axiomatizability axiomatization axiomatizations axiomatizing bagging baire-space baker-map banach-lattice banach-space basis bayesian bayesian-network bayesian-sequence-prediction behavior behavioral behavioral-rewriting behavior-space behaviour belief-networks beliefs benchmark benford-law besov besov-space betting bianchi-classification bias bibliography bidirectionality bifurcation binary binary-dihedral-groups binary-icosahedral-group binary-icosahedral-space binary-octahedral-group binary-octahedral-space binary-physics binary-tetrahedral-group binary-tetrahedral-space biodiversity biology biophysics biops bisimulation bitmap bit-string bit-string-physics black-hole blending-theory blend-space blockworld boolean-algebra boolean-dissimilarity boosting bootstrapping bottom-up boundary bounded-complete-models bounds branching branching-time branching-time-temporal-logic branes breaking browser browsing budgeting business business-development business-model business-process business-process-space business-rules buy-and-hold bv by-example ca caching cad calculation calculational calculational-proofs calculus calculus-of-constructions calculus-of-structures calendar c-algebra c-algebras call-graph caml canonical-correlation-analysis cantor-set cantor-space capacity capm carcinogenesis cardinality cartesian-closed-categories cascade case-based case-based-reasoning cash-flow casimir-effect casl catastrophe-theory categorial categorial-theories categorical categorical-abstract-algebraic-logic categorical-abstract-machine categorical-logic categorical-models categorical-model-theory categorical-proof-theory categorical-semantics categorical-systems-theory categorical-theories categorification categorified-algebra categorization category category-of-algebras category-of-categories category-of-complete-lattices category-of-formal-contexts category-of-fuzzy-sets category-of-ideals category-of-information-systems category-of-languages category-of-modules category-of-patents category-of-posets category-of-programs category-of-signatures category-of-specifications category-of-structure-types category-of-stuff-types category-of-systems category-of-theories category-theory cathegory-theory causality causal-minimisation causal-state-machine cavity cbr ccp cct cellular cellular-automata cellular-network centralized central-limit-theorem cg chains change channel-theory chaos chaos-control chaos-theory chaotic chaotic-wave-function charters checking chemical chemistry chip-firing-games chronological-minimisation chu chu-space cip circuitry citation citations class-hierarchy classicality classical-limit classical-logic classical-phase-space classification classification-rules classifier classifying-categories clifford-algebra climate clique cliques clocked-transition-system closed-categories closure closure-lattice closure-space closure-structures clp cluster- clustering clusteringstreams cmb coalgebra coalition coalition-formation coarse-graining code code-space coding coding-theory coevolution co-evolution coevolving cognition cognitive-agents cognitive-computing coherence coherence-analysis coherent-state coinductive-rewriting colimit collaboration collaborative collaborative-argumentation collaborative-filtering collaborative-problem-solving collective collision collision-detection combination combinatorial combinatorics combinators combinatory-logic combining committed-choice common-lisp common-sense communication communities community commutative commutativity comonotonicity compact-metric-space compactness comparison compensation competition competitive compiler compiling complementarity complete complete-axiomatization completeness complete-partial-order completion complex-dimensions complexity complexity-oscillations complexity-theory complextity component components composing composite-kernel composite-web-service composition compositionality compoundness compressibility compressing compression compuatational-structures computability computability-logic computability-theory computable computable-analysis computable-language computable-structures computation computational computational-algebraic-geometry computational-biology computational-category-theory computational-complexity computational-cosmology computational-economics computational-effects computational-eistemology computational-epistemology computational-finance computational-learning computational-legal-sciences computational-logic computational-mathematics computational-mechanics computational-model-theory computational-narratology computational-neuroscience computational-physics computational-science computational-semiotics computational-sociology computational-statistics computational-structures computational-structure-theory computational-universality computing concept concept-formation concept-lattice concept-map concept-programming conceptual conceptual-space conceptual-structures concurrency concurrent conditionality conditional-probability conditioning configuration configuration-space configuration-structures confinement conflict conformal confusability-matrix conjecture connectedness connection connectionism consciousness consensus conservation consistency constant constraint constraints construction constructive constructive-category-theory constructive-hausdorff-dimension constructive-logic constructive-proof consumption context context-logic context-model context-relativity context-selection contextuality contextualization contextual-reasoning contimuum continued-fraction continuity continuous continuous-information-system continuous-query contracting contracts contradiction contravariance control control-flow control-flow-graph control-language convexity cooperation cooperative coordination coordinator corpus corrections correlation correlations correspondence corruption cosmological-constant cosmological-parameters cosmological-scale cosmological-theory cosmology cost costing countability counterexample counter-example counterexamples coupled coupling covariance cpo crash creativity crisis critical-behavior critical-exponent criticality critical-path critical-path-horizon critical-phenomena critical-phenomenon critics crosscutting cross-product crowdsourcing csp ct cultrual-evolution cultural-evolution culture cumulator curry-howard curry-howard-isomorphism curvature curve cybernetics cyclic-groups dag data database database-of-categories data-detector data-mining data-model datrix db dcsp deadlock debugging decategorification decentralized decidability decidable decidable-structures decidable-theories deciding decision decision-diagram decision-procedure decision-support decision-theory decision-tree declarative-programming decoherence decomposition decompressibility decompressing deduction deep-inference default default-logic default-reasoning default-theory defeasibility defeasible defeasible-logic defect definability deforestation deformation delay delocalization delooping democracy dendrogram dependency derivation derivative derived-categories description descriptive-complexity design design-lattice design-process design-space design-theory desires desktop desynchronization detection detector determinism detrended-fluctuation-analysis dev development development-graph diagonalization diagram diagram-chasing diagrammatic diagrammatic-inference diagrammatic-reasoning dialgebra dialogue diffeomorphism differential-equations differential-geometry diffusion diffusion-waves digital-circuits digital-library digraph dilemma dimension dimensional-analysis dimensionality dimensionality-reduction dimensional-stacking dimension-theory directed-percolation direct-inference direct-manipulation disambiguation discourse discovery discrete discrete-differential-geometry discrete-geometry discreteness discrete-scale-invariance discrete-self-similarity discrete-space discrete-time-mechanics discretization disjunctive-sequences disorder disordering dissimilarity dissipative distance distance-lattice distance-matrix distinguishability distrbution distributed distribution distributional-semantics distributive-lattice distributivity divergence diversity divide-and-conquer divisibility dl dla dna document document-development dodecahedral dodecahedral-space domain-logic domains domain-selection domain-theory dominance double-pareto-distribution double-pareto-lognormal-distribution drafting drift dsms dt dual-ideals duality dynamic dynamic-algebras dynamical-invariants dynamically-expanding-context dynamical-system dynamic-analysis dynamics ea earthquake ebusiness e-business ecology economics economic-space econophysics editor edutainment effect effective-model-theory effective-topos effects efficiency eigenmode eigenmodes eigenproblem eigenvalue eigenvector eis elementary-particles embeddedness embedding embedding-theorem embedment emergence emergent empty-set endogeneous endogenous end-user-programming energy engineering enriched-category enriched-category-theory enrichment ensemble entailment-relation entanglement enterprise enterprise-portfolio entropy entropy-change enumerability enumerative environment eom epimorphism epistemology epsilonmachine epsilon-machine equation equational equational-logic equations equilibrium equilogical-space equivalence equivalence-class ergodicity ergonomics error e-science estimating evaluation evaluator event events event-space event-structure event-structures evidence evolution evolutionary evolutionary-spectral-analysis evolvability evolving evolving-algebras executability executable executable-model executing execution