1 resultado para Checking accounts
em AMS Tesi di Dottorato - Alm@DL - Università di Bologna
Filtro por publicador
- Repository Napier (1)
- Aberdeen University (5)
- Academic Research Repository at Institute of Developing Economies (1)
- Acceda, el repositorio institucional de la Universidad de Las Palmas de Gran Canaria. España (3)
- AMS Tesi di Dottorato - Alm@DL - Università di Bologna (1)
- Aquatic Commons (1)
- Archive of European Integration (353)
- Aston University Research Archive (15)
- Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (4)
- Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (BDPI/USP) (2)
- Biblioteca Digital de la Universidad Católica Argentina (1)
- Biblioteca Digital de Teses e Dissertações Eletrônicas da UERJ (1)
- Biodiversity Heritage Library, United States (1)
- BORIS: Bern Open Repository and Information System - Berna - Suiça (14)
- Boston University Digital Common (3)
- Brock University, Canada (37)
- Bulgarian Digital Mathematics Library at IMI-BAS (2)
- Cambridge University Engineering Department Publications Database (6)
- CentAUR: Central Archive University of Reading - UK (12)
- Center for Jewish History Digital Collections (7)
- Chinese Academy of Sciences Institutional Repositories Grid Portal (6)
- Collection Of Biostatistics Research Archive (2)
- Comissão Econômica para a América Latina e o Caribe (CEPAL) (36)
- CORA - Cork Open Research Archive - University College Cork - Ireland (4)
- Dalarna University College Electronic Archive (2)
- Deakin Research Online - Australia (28)
- Digital Commons @ Center for the Blue Economy - Middlebury Institute of International Studies at Monterey (2)
- Digital Peer Publishing (1)
- Doria (National Library of Finland DSpace Services) - National Library of Finland, Finland (1)
- eResearch Archive - Queensland Department of Agriculture; Fisheries and Forestry (1)
- Greenwich Academic Literature Archive - UK (2)
- Harvard University (21)
- Helda - Digital Repository of University of Helsinki (2)
- Indian Institute of Science - Bangalore - Índia (7)
- Ministerio de Cultura, Spain (2)
- National Center for Biotechnology Information - NCBI (3)
- Nottingham eTheses (2)
- Ohio University (2)
- Plymouth Marine Science Electronic Archive (PlyMSEA) (2)
- Portal de Revistas Científicas Complutenses - Espanha (1)
- QUB Research Portal - Research Directory and Institutional Repository for Queen's University Belfast (25)
- Queensland University of Technology - ePrints Archive (93)
- RDBU - Repositório Digital da Biblioteca da Unisinos (1)
- Repositório digital da Fundação Getúlio Vargas - FGV (1)
- Repositório Institucional UNESP - Universidade Estadual Paulista "Julio de Mesquita Filho" (2)
- Research Open Access Repository of the University of East London. (2)
- RUN (Repositório da Universidade Nova de Lisboa) - FCT (Faculdade de Cienecias e Technologia), Universidade Nova de Lisboa (UNL), Portugal (1)
- School of Medicine, Washington University, United States (29)
- South Carolina State Documents Depository (2)
- Universidad de Alicante (1)
- Universidad Politécnica de Madrid (6)
- Universidade Técnica de Lisboa (1)
- Université de Montréal, Canada (2)
- University of Michigan (181)
- University of Queensland eSpace - Australia (15)
- University of Southampton, United Kingdom (1)
- WestminsterResearch - UK (2)
Resumo:
The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement. It is a central piece of compilers and proof assistants. We postulate that since type checkers are at the interface between proof theory and program theory, their study can let these two fields mutually enrich each other. We argue by two main instances: first, starting from the problem of proof reuse, we develop an incremental type checker; secondly, starting from a type checking program, we evidence a novel correspondence between natural deduction and the sequent calculus.