Fusion in Coq (577 views)
Lecture Notes In Computer Science (ISSN: 0302-9743, 0302-974335404636319783540463634, 0302-974335402975459783540297543), 2001; 2178LNCS: 583-596.
Export to BibTeX Export to EndNote
Paper type: Journal Article,
Impact factor: 0.415, 5-year impact factor: 0
Url: http://www.scopus.com/inward/record.url?eid=2-s2.0-35048815731&partnerID=40&md5=ae158650a437b6e54cf1d735c1667b8a
Keywords: Constructive Proof, Dependent Types, Generalisation, Inductive-Type, Morphisms, Optimisations, Parametric Polymorphism, Recursive Types, Artificial Intelligence, Computer Science, System Theory, Beta Interferon, Cell Surface Protein, Immunoglobulin Enhancer Binding Protein, Interleukin 10, Mitogen Activated Protein Kinase, Virus Fusion Protein, Article, Cell Membrane, Controlled Study, Cytokine Production, Enzyme Linked Immunosorbent Assay, Filoviridae, Flavivirus, Human, Human Cell, Immunoprecipitation, In Vitro Study, Nonhuman, Orthomyxovirus, Paramyxovirus, Priority Journal, Protein Domain, Protein Interaction, Protein Phosphorylation, Protein Synthesis, Retrovirus, Rhabdovirus, Signal Transduction, Solid Phase Synthesis, Src Homology Domain, Strain Difference, Togavirus, Virus Entry, Virus Strain, Western Blotting, Cell Line, Enzyme-Linked Immunosorbent Assay, Host-Pathogen Interactions, Interferon-Beta, Interleukin-10, Monocytes, Transcriptional Activation, Viral Fusion Proteins,
Affiliations:
*** IBB - CNR ***
LFCIA, Dpt. of Computer Science, University of A Coruna, 15071 A Coruna, Spain
IES Carballo Calero, Avda. Castelao, 15406 Ferrol, Spain, Spain
Department of Experimental Medicine, Section of Microbiology and Clinical Microbiology, Second University of Naples, IT-80138 Naples, Italy
Department of Biological Sciences, University of Naples 'Federico II', Institute of Biostructures and Bioimaging, Naples, Italy
References:
Not available.
Lecture Notes In Computer Science (ISSN: 0302-9743, 0302-974335404636319783540463634, 0302-974335402975459783540297543), 2001; 2178LNCS: 583-596.
Export to BibTeX Export to EndNote
Paper type: Journal Article,
Impact factor: 0.415, 5-year impact factor: 0
Url: http://www.scopus.com/inward/record.url?eid=2-s2.0-35048815731&partnerID=40&md5=ae158650a437b6e54cf1d735c1667b8a
Keywords: Constructive Proof, Dependent Types, Generalisation, Inductive-Type, Morphisms, Optimisations, Parametric Polymorphism, Recursive Types, Artificial Intelligence, Computer Science, System Theory, Beta Interferon, Cell Surface Protein, Immunoglobulin Enhancer Binding Protein, Interleukin 10, Mitogen Activated Protein Kinase, Virus Fusion Protein, Article, Cell Membrane, Controlled Study, Cytokine Production, Enzyme Linked Immunosorbent Assay, Filoviridae, Flavivirus, Human, Human Cell, Immunoprecipitation, In Vitro Study, Nonhuman, Orthomyxovirus, Paramyxovirus, Priority Journal, Protein Domain, Protein Interaction, Protein Phosphorylation, Protein Synthesis, Retrovirus, Rhabdovirus, Signal Transduction, Solid Phase Synthesis, Src Homology Domain, Strain Difference, Togavirus, Virus Entry, Virus Strain, Western Blotting, Cell Line, Enzyme-Linked Immunosorbent Assay, Host-Pathogen Interactions, Interferon-Beta, Interleukin-10, Monocytes, Transcriptional Activation, Viral Fusion Proteins,
Affiliations:
*** IBB - CNR ***
LFCIA, Dpt. of Computer Science, University of A Coruna, 15071 A Coruna, Spain
IES Carballo Calero, Avda. Castelao, 15406 Ferrol, Spain, Spain
Department of Experimental Medicine, Section of Microbiology and Clinical Microbiology, Second University of Naples, IT-80138 Naples, Italy
Department of Biological Sciences, University of Naples 'Federico II', Institute of Biostructures and Bioimaging, Naples, Italy
References:
Not available.
Fusion in Coq
Fusion theorem is a classical result that allows the simplification of the morphisms among homogeneus structures [10]. We present this theorem and some generalizations in the context of the constructive proof assistant tool Coq [2] where we have dependent types and parametric polymorphism. The work is organised as follows: afther the classical interpretation of the fusion law for catamorphisms in a categoric context, examples of fusion for programs defined with recursive types in Coq are analysed and the theorems of corresponding optimisation are shown. Finally, a generalisation of fusion law for inductive types is presented which is applied to a specific case. © 2011 Springer-Verlag Berlin Heidelberg.
Fusion theorem is a classical result that allows the simplification of the morphisms among homogeneus structures [10]. We present this theorem and some generalizations in the context of the constructive proof assistant tool Coq [2] where we have dependent types and parametric polymorphism. The work is organised as follows: afther the classical interpretation of the fusion law for catamorphisms in a categoric context, examples of fusion for programs defined with recursive types in Coq are analysed and the theorems of corresponding optimisation are shown. Finally, a generalisation of fusion law for inductive types is presented which is applied to a specific case. © 2011 Springer-Verlag Berlin Heidelberg.
Fusion in Coq
No results. |
Fusion in Coq
Other filter: ([btitle,keywords] "Constructive Proof" ...
Molko N, Pappata S, Mangin JF, Poupon C, Vahedi K, Jobert A, LeBihan D, Bousser MG, Chabriat H
* Diffusion tensor imaging study of subcortical gray matter in CADASIL (726 views)
Stroke (ISSN: 0039-2499), 2001 Sep; 32(9): 2049-2054.
Impact Factor: 5.33
View Export to BibTeX Export to EndNote
* Diffusion tensor imaging study of subcortical gray matter in CADASIL (726 views)
Stroke (ISSN: 0039-2499), 2001 Sep; 32(9): 2049-2054.
Impact Factor: 5.33
View Export to BibTeX Export to EndNote
1 Records (1 excluding Abstracts).
Total impact factor: 5.33 (5.33 excluding Abstracts).
Total 5 year impact factor: 6.757 (6.757 excluding Abstracts).
Total impact factor: 5.33 (5.33 excluding Abstracts).
Total 5 year impact factor: 6.757 (6.757 excluding Abstracts).
577 views. Last view on Saturday 21 September 2024, 18:57:11
ibb.cnr.it
