Generic Programming within Dependently Typed Programming

Name: Work Video:
Duration: 3 min 30 s
Description: We show how higher kinded generic programming can be represented faithfully within a dependently typed programming system. This development has been implemented using the Oleg system. The present work can be seen as evidence for our thesis that extensions of type systems can be done by programming within a dependently typed language, using data as codes for types.
Thorsten Altenkirch; Conor McBride
{'id': 'https://openalex.org/W1578113853', 'doi': 'https://doi.org/10.1007/978-0-387-35672-3_1', 'title': 'Generic Programming within Dependently Typed Programming', 'display_name': 'Generic Programming within Dependently Typed Programming', 'publication_year': 2003, 'publication_date': '2003-01-01', 'ids': {'openalex': 'https://openalex.org/W1578113853', 'doi': 'https://doi.org/10.1007/978-0-387-35672-3_1', 'mag': '1578113853'}, 'language': 'en', 'primary_location': {'is_oa': True, 'landing_page_url': 'https://doi.org/10.1007/978-0-387-35672-3_1', 'pdf_url': 'https://link.springer.com/content/pdf/10.1007/978-0-387-35672-3_1.pdf', 'source': {'id': 'https://openalex.org/S4210185096', 'display_name': 'IFIP advances in information and communication technology', 'issn_l': '1868-4238', 'issn': ['1868-4238', '1868-422X'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319900', 'host_organization_name': 'Springer Science+Business Media', 'host_organization_lineage': ['https://openalex.org/P4310319965', 'https://openalex.org/P4310319900'], 'host_organization_lineage_names': ['Springer Nature', 'Springer Science+Business Media'], 'type': 'book series'}, 'license': 'other-oa', 'license_id': 'https://openalex.org/licenses/other-oa', 'version': 'publishedVersion', 'is_accepted': True, 'is_published': True}, 'type': 'book-chapter', 'type_crossref': 'book-chapter', 'indexed_in': ['crossref'], 'open_access': {'is_oa': True, 'oa_status': 'hybrid', 'oa_url': 'https://link.springer.com/content/pdf/10.1007/978-0-387-35672-3_1.pdf', 'any_repository_has_fulltext': False}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5056420469', 'display_name': 'Thorsten Altenkirch', 'orcid': 'https://orcid.org/0000-0002-6582-5025'}, 'institutions': [{'id': 'https://openalex.org/I142263535', 'display_name': 'University of Nottingham', 'ror': 'https://ror.org/01ee9ar58', 'country_code': 'GB', 'type': 'education', 'lineage': ['https://openalex.org/I142263535']}], 'countries': ['GB'], 'is_corresponding': False, 'raw_author_name': 'Thorsten Altenkirch', 'raw_affiliation_strings': ['School of Computer Science and Information Technology, University of Nottingham, Wollaton Road, Nottingham, NG8 1BB, UK'], 'affiliations': [{'raw_affiliation_string': 'School of Computer Science and Information Technology, University of Nottingham, Wollaton Road, Nottingham, NG8 1BB, UK', 'institution_ids': ['https://openalex.org/I142263535']}]}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5090954120', 'display_name': 'Conor McBride', 'orcid': 'https://orcid.org/0000-0003-1487-0886'}, 'institutions': [{'id': 'https://openalex.org/I190082696', 'display_name': 'Durham University', 'ror': 'https://ror.org/01v29qb04', 'country_code': 'GB', 'type': 'education', 'lineage': ['https://openalex.org/I190082696']}], 'countries': ['GB'], 'is_corresponding': False, 'raw_author_name': 'Conor Mcbride', 'raw_affiliation_strings': ['Department of Computer Science, University of Durham, South Road, Durham, DH1 3LE, UK'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, University of Durham, South Road, Durham, DH1 3LE, UK', 'institution_ids': ['https://openalex.org/I190082696']}]}], 'institution_assertions': [], 'countries_distinct_count': 1, 'institutions_distinct_count': 2, 'corresponding_author_ids': [], 'corresponding_institution_ids': [], 'apc_list': None, 'apc_paid': None, 'fwci': 5.345, 'has_fulltext': True, 'fulltext_origin': 'pdf', 'cited_by_count': 94, 'citation_normalized_percentile': {'value': 0.969799, 'is_in_top_1_percent': False, 'is_in_top_10_percent': True}, 'cited_by_percentile_year': {'min': 95, 'max': 96}, 'biblio': {'volume': None, 'issue': None, 'first_page': '1', 'last_page': '20'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10126', 'display_name': 'Logic, programming, and type systems', 'score': 0.9998, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, 'topics': [{'id': 'https://openalex.org/T10126', 'display_name': 'Logic, programming, and type systems', 'score': 0.9998, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T11010', 'display_name': 'Logic, Reasoning, and Knowledge', 'score': 0.9947, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T12002', 'display_name': 'Computability, Logic, AI Algorithms', 'score': 0.9842, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}], 'keywords': [{'id': 'https://openalex.org/keywords/generic-programming', 'display_name': 'Generic programming', 'score': 0.5998162}, {'id': 'https://openalex.org/keywords/data-type', 'display_name': 'Data type', 'score': 0.4244863}], 'concepts': [{'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.81464684}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.72269064}, {'id': 'https://openalex.org/C7051814', 'wikidata': 'https://www.wikidata.org/wiki/Q1051282', 'display_name': 'Generic programming', 'level': 2, 'score': 0.5998162}, {'id': 'https://openalex.org/C34165917', 'wikidata': 'https://www.wikidata.org/wiki/Q188267', 'display_name': 'Programming paradigm', 'level': 2, 'score': 0.5272452}, {'id': 'https://openalex.org/C96315309', 'wikidata': 'https://www.wikidata.org/wiki/Q5508829', 'display_name': 'Functional logic programming', 'level': 4, 'score': 0.5236273}, {'id': 'https://openalex.org/C119263510', 'wikidata': 'https://www.wikidata.org/wiki/Q7248501', 'display_name': 'Programming domain', 'level': 4, 'score': 0.47360277}, {'id': 'https://openalex.org/C50033165', 'wikidata': 'https://www.wikidata.org/wiki/Q15712089', 'display_name': 'Inductive programming', 'level': 3, 'score': 0.4466201}, {'id': 'https://openalex.org/C146206909', 'wikidata': 'https://www.wikidata.org/wiki/Q531152', 'display_name': 'Declarative programming', 'level': 4, 'score': 0.4346551}, {'id': 'https://openalex.org/C120558287', 'wikidata': 'https://www.wikidata.org/wiki/Q1418502', 'display_name': 'Procedural programming', 'level': 4, 'score': 0.426647}, {'id': 'https://openalex.org/C138958017', 'wikidata': 'https://www.wikidata.org/wiki/Q190087', 'display_name': 'Data type', 'level': 2, 'score': 0.4244863}, {'id': 'https://openalex.org/C150762246', 'wikidata': 'https://www.wikidata.org/wiki/Q4354073', 'display_name': 'Reactive programming', 'level': 4, 'score': 0.42139393}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': True, 'landing_page_url': 'https://doi.org/10.1007/978-0-387-35672-3_1', 'pdf_url': 'https://link.springer.com/content/pdf/10.1007/978-0-387-35672-3_1.pdf', 'source': {'id': 'https://openalex.org/S4210185096', 'display_name': 'IFIP advances in information and communication technology', 'issn_l': '1868-4238', 'issn': ['1868-4238', '1868-422X'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319900', 'host_organization_name': 'Springer Science+Business Media', 'host_organization_lineage': ['https://openalex.org/P4310319965', 'https://openalex.org/P4310319900'], 'host_organization_lineage_names': ['Springer Nature', 'Springer Science+Business Media'], 'type': 'book series'}, 'license': 'other-oa', 'license_id': 'https://openalex.org/licenses/other-oa', 'version': 'publishedVersion', 'is_accepted': True, 'is_published': True}], 'best_oa_location': {'is_oa': True, 'landing_page_url': 'https://doi.org/10.1007/978-0-387-35672-3_1', 'pdf_url': 'https://link.springer.com/content/pdf/10.1007/978-0-387-35672-3_1.pdf', 'source': {'id': 'https://openalex.org/S4210185096', 'display_name': 'IFIP advances in information and communication technology', 'issn_l': '1868-4238', 'issn': ['1868-4238', '1868-422X'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319900', 'host_organization_name': 'Springer Science+Business Media', 'host_organization_lineage': ['https://openalex.org/P4310319965', 'https://openalex.org/P4310319900'], 'host_organization_lineage_names': ['Springer Nature', 'Springer Science+Business Media'], 'type': 'book series'}, 'license': 'other-oa', 'license_id': 'https://openalex.org/licenses/other-oa', 'version': 'publishedVersion', 'is_accepted': True, 'is_published': True}, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 27, 'referenced_works': ['https://openalex.org/W1503362807', 'https://openalex.org/W1506492451', 'https://openalex.org/W1511133369', 'https://openalex.org/W1557825595', 'https://openalex.org/W1578113853', 'https://openalex.org/W1587287586', 'https://openalex.org/W1601722070', 'https://openalex.org/W1846463844', 'https://openalex.org/W1905449393', 'https://openalex.org/W1964211642', 'https://openalex.org/W1979323701', 'https://openalex.org/W1995675054', 'https://openalex.org/W2027584005', 'https://openalex.org/W2058137890', 'https://openalex.org/W2072137506', 'https://openalex.org/W2078334802', 'https://openalex.org/W2114980032', 'https://openalex.org/W2117477507', 'https://openalex.org/W2123360309', 'https://openalex.org/W2175912519', 'https://openalex.org/W2493130382', 'https://openalex.org/W2522041776', 'https://openalex.org/W2911433283', 'https://openalex.org/W3014278192', 'https://openalex.org/W4252656082', 'https://openalex.org/W569543113', 'https://openalex.org/W975212003'], 'related_works': ['https://openalex.org/W4248653691', 'https://openalex.org/W27046826', 'https://openalex.org/W2560787608', 'https://openalex.org/W2393528030', 'https://openalex.org/W2296381500', 'https://openalex.org/W2189001763', 'https://openalex.org/W2172209430', 'https://openalex.org/W2161156675', 'https://openalex.org/W2039406101', 'https://openalex.org/W1828224469'], 'abstract_inverted_index': {'We': [0], 'show': [1], 'how': [2], 'higher': [3], 'kinded': [4], 'generic': [5], 'programming': [6, 15, 46], 'can': [7, 29, 42], 'be': [8, 30, 43], 'represented': [9], 'faithfully': [10], 'within': [11, 47], 'a': [12, 48], 'dependently': [13, 49], 'typed': [14, 50], 'system.': [16, 25], 'This': [17], 'development': [18], 'has': [19], 'been': [20], 'implemented': [21], 'using': [22, 52], 'the': [23], 'Oleg': [24], 'The': [26], 'present': [27], 'work': [28], 'seen': [31], 'as': [32, 54], 'evidence': [33], 'for': [34, 56], 'our': [35], 'thesis': [36], 'that': [37], 'extensions': [38], 'of': [39], 'type': [40], 'systems': [41], 'done': [44], 'by': [45], 'language,': [51], 'data': [53], 'codes': [55], 'types.': [57]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W1578113853', 'counts_by_year': [{'year': 2022, 'cited_by_count': 2}, {'year': 2021, 'cited_by_count': 2}, {'year': 2020, 'cited_by_count': 3}, {'year': 2019, 'cited_by_count': 3}, {'year': 2018, 'cited_by_count': 4}, {'year': 2017, 'cited_by_count': 4}, {'year': 2016, 'cited_by_count': 4}, {'year': 2015, 'cited_by_count': 3}, {'year': 2014, 'cited_by_count': 2}, {'year': 2013, 'cited_by_count': 8}, {'year': 2012, 'cited_by_count': 3}], 'updated_date': '2024-12-13T02:33:55.390455', 'created_date': '2016-06-24'}
Publication Information

Basic Information

Access and Citation

AI Researcher Chatbot

Primary Location

Authors

Topics

Keywords

Related Works
