Blockchain Papers

Follow blockchain research across journals, conferences, and preprint repositories.

126 papersLast indexed Aug 31, 2026
Search papers

Paper index

126 results ¡ page 5 of 6

Clear filters
Aug 26, 2011¡Inter-American Development Bank
0 cites
Country Program Evaluation: Colombia (2007-2010)

Jorge F. Chåvez, Roberto F. Iunes, Hector Conroy, Johanna Ramos ¡ 7 authors

This evaluation examines the IDB's Country Program with Colombia for the 2007-2011 period. The evaluation found social investment and decentralization as two areas in which the IDB maintained presence and relevance during this period. In social investment, the IDB was consolidated as a stable partner to Colombia in the creation and operation of a long-term social safety net. In regards to decentralization, cooperation was crosscutting, as the IDB worked with subnational institutions in diverse sectors, such as transportation, business development, housing, and modernization of the State. The IDB also continued its long-term work with Colombia to modernize and improve the efficiency of oversight agencies and the judicial branch, helping the country to obtain sizeable savings. To continue to improve the strategy with Colombia, OVE recommends that the IDB should: (i) increase its efforts to lower the transaction costs of IDB's cooperation with the country; (ii) improve the evaluability, monitoring and evaluation of the Country Strategy and the projects financed by the IDB; (iii) identify and strengthen the IDB's capacity in the areas and sectors in which the country will concentrate its demand for financial cooperation; and (iv) identify international development experiences that have been successful and present them to Colombia.

Open access
Hermeneutics and Narrative Identity
Aging, Elder Care, and Social Issues
Health, Medicine and Society
Original source
Jan 1, 2010¡Studia Europaea Gnesnensia
0 cites
W poszukiwaniu miejsca Ukrainy na kulturalnej mapie Europy. Ukraińskie dyskusje literackie lat 20. XX wieku

Albert Nowacki

According to a contemporary Pole, Ukraine is a country which, having broken out of the clutches of communism, makes its way towards Europe, the place it has always belonged to. The proof of that are the Ukrainians’ European aspirations—to become a member of the EU or NATO, as well as the events of the Orange Revolution, which proved that Ukrainians are mature enough to break free from Russia for the sake of democratization of the country, following the example of Western European countries. However, Ukrainians themselves are no longer so unanimous. A careful look at the country of our neighbours makes it evident that both in the sphere of politics as well as culture the Ukrainian nation is strongly divided. This was demonstrated by the Orange Revolution, which made the West realise that in Ukraine a fight is taking place, where the choice of an eastern or western variant is at stake. Ukrainians are also divided as far as their identity is concerned, both cultural and national, for whose roots they are still searching, both in Russia and Western Europe. We may say that as far as the matter of their place on earth is concerned, Ukrainians are almost in exactly the same place as they were eighty years ago.

Open access
Hermeneutics and Narrative Identity
Aging, Elder Care, and Social Issues
Health, Medicine and Society
Original source
Aug 1, 2009¡2009 Symposium on Bio-inspired Learning and Intelligent Systems for Security
10 cites
Autonomous Physical Secret Functions and Clone-Resistant Identification

Wael Adi

Self configuring VLSI technology architectures offer a new environment for creating novel security functions. Two such functions for physical security architectures are proposed to be generated autonomously as unknown/secret internal functions. A cell-based FPGA technology architecture is deployed for generating two classes of self-constructed one-way physical secret functions, one representing a hash function and the other a ciphering function. The Hash function is a non-invertible mapping, where the cipher function should be invertible. The two sample architectures of the functions are inspired from the programmable cell structure of the selected FPGA technology. As the functions are internally created, their mapping structures can be kept completely secret and even unknown to anybody. Such units could be efficiently deployed for a novel physical security even when nothing is known about their exact architecture and mapping functions. Several new attractive application scenarios are demonstrated including a type of zero-knowledge proof of identity and clone-resistant physical units as well as secured dependency functions. It is also shown that such security mechanisms can be kept operational for some useful applications even if the secret-unknown functions are allowed to evolve and develop additional time-dependent and individual properties. Such security functions became recently possible after self-configuring VLSI architectures are available as a part of real microelectronic systems. Keywords-Identification; secret unknown hardware functions; clone-resitant units; secret-unknown physicalcipher, secret unknown hash-functions. 1.

2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Cryptographic Implementations and Security
Advanced Memory and Neural Computing
Original source
Jan 1, 2005¡Lecture notes in computer science
8 cites
Dropout-Tolerant TTP-Free Mental Poker

Jordi Castellà‐Roca, Francesc Sebé, Josep Domingo‐Ferrer

Abstract. There is a broad literature on distributed card games over communications networks, collectively known as mental poker. Likein any distributed protocol, avoiding the need for a Trusted Third Party (TTP) in mental poker is highly desirable, because really trusted TTPs are not always available and seldom free. This paper deals with the player dropout problem in mental poker without a TTP. A solution based on zero-knowledge proofs is proposed. While staying TTP-free, our proposal allows the game to continue after player dropout.

2 source records
Peer-to-Peer Network Technologies
Cryptography and Data Security
Blockchain Technology Applications and Security
Original source
Jan 1, 2005¡Lecture notes in computer science
39 cites
3-Move Undeniable Signature Scheme

Kaoru Kurosawa, Swee‐Huay Heng

Abstract. In undeniable signature schemes, zero-knowledgeness and non-transferability have been identified so far. In this paper, by separating these two notions, we show the first 3-move confirmation and disavowal protocols for Chaum’s undeniable signature scheme which is secure against active and concurrent attacks. Our main observation is that while the signer has one public key and one secret key, there exist two witnesses in the confirmation and disavowal proofs of Chaum’s scheme.

Open access
2 source records
Cryptography and Data Security
Blockchain Technology Applications and Security
Complexity and Algorithms in Graphs
Original source
Jan 1, 2005¡Lecture notes in computer science
57 cites
Updatable Zero-Knowledge Databases

Moses Liskov

Abstract. Micali, Rabin, and Kilian [9] recently introduced zero-knowledge sets and databases, in which a prover sets up a database by publishing a commitment, and then gives proofs about particular values. While an elegant and useful primitive, zero-knowledge databases do not offer any good way to perform updates. We explore the issue of updating zero-knowledge databases. We define and discuss transparent updates, which (1) allow holders of proofs that are still valid to update their proofs, but (2) otherwise maintain secrecy about the update. We give rigorous definitions for transparently updatable zero-knowledge databases, and give a practical construction based on the Chase et al [2] construction, assuming that verifiable random functions exist and that mercurial commitments exist, in the random oracle model. We also investigate the idea of updatable commitments, an attempt to make simple commitments transparently updatable. We define this new primitive and give a simple secure construction.

2 source records
Cryptography and Data Security
Privacy-Preserving Technologies in Data
Cloud Data Security Solutions
Original source
Jan 1, 2005¡Lecture notes in computer science
32 cites
Efficient Designated Confirmer Signatures Without Random Oracles or General Zero-Knowledge Proofs

Craig Gentry, DĂĄvid MolnĂĄr, Zulfikar Ramzan

Abstract. Most prior designated confirmer signature schemes either prove security in the random oracle model (ROM) or use general zeroknowledge proofs for NP statements (making them impractical). By slightly modifying the definition of designated confirmer signatures, Goldwasser and Waisbard presented an approach in which the Confirm and ConfirmedSign protocols could be implemented without appealing to general zero-knowledge proofs for NP statements (their Disavow protocol still requires them). The Goldwasser-Waisbard approach could be instantiated using Cramer-Shoup, GMR, or Gennaro-Halevi-Rabin signatures. In this paper, we provide an alternate generic transformation to convert any signature scheme into a designated confirmer signature scheme, without adding random oracles. Our key technique involves the use of a signature on a commitment and a separate encryption of the random string used for commitment. By adding this “layer of indirection, ” the underlying protocols in our schemes admit efficient instantiations (i.e., we can avoid appealing to general zero-knowledge proofs for NP statements) and furthermore the performance of these protocols is not tied to the choice of underlying signature scheme. We illustrate this using the Camenisch-Shoup variation on Paillier’s cryptosystem and Pedersen commitments. The confirm protocol in our resulting scheme requires 10 modular exponentiations (compared to 320 for Goldwasser-Waisbard) and our disavow protocol requires 41 modular exponentiations (compared to using a general zero-knowledge proof for Goldwasser-Waisbard). Previous schemes use the encryption of a signature paradigm, and thus run into problems when trying to implement the confirm and disavow protocols efficiently. 1

Open access
2 source records
Cryptography and Data Security
Advanced Authentication Protocols Security
Oral and gingival health research
Original source
Dec 1, 2004¡Psychogeriatrics
1 cites
Health‐care system in France

Olivier Saint‐Jean

The French health-care system is almost totally under the supervision of the government, which defines the general orientation of health policy. For example, a health-care policy for cancer treatment will be developed in France within the next 5 years. The government organizes the initial formation of all categories of health professionals and so controls the number of professionals in each category. In France, 4500 medical students graduate each year. Demographic problems at the present time are caused by the quota for all medical professions. The government also ensures that the number and location of hospitals are adequate for the needs of the French population. It supervises public hospitals and the management of private clinics, with the objective of providing a consistent standard of care in all health-care structures. The government also proposes the health budget for parliament's approval. In 1996, in line with the concept of decentralization, which means ‘to think globally but act locally’, regional agencies for hospital care were created in each administrative region. They are responsible for the strategic and economic supervision of hospitals, and for the organization of regional health care. However, they have no authority with regard to ambulatory care, thus creating a gap between hospital and ambulatory care in France, which represents a great obstacle to the coordination of care for disabled and elderly people. The French health-care system is a mixed system, being both etatic and liberal. There is a collective health insurance program in place based on incomes; the premium payments are automatically deducted from salaries. The rate is determined each year by the government for an equilibrated budget. Patients have completely free access to all medical care, including hospitals and choice of practitioners. They can have as many consultations and hospitalizations as they want. Furthermore, public and private health structures coexist. Sixty-five percent of hospitals are public and 35% are private. Ambulatory care structures are mainly private (95%). Therefore, although the French system is complex, comprising etatic and private organizations, it functions well. Furthermore, freedom and heterogeneity are probably the main guarantees of quality of health care in France, even if the cost is high and constantly increasing. In France, the number of available hospital beds for acute care (short-stay units), rehabilitation, long-term care and psychiatry is high (Table 1). The rates per 1000 people are the highest in Europe. However, the number of beds for disabled geriatric patients is low: 400 000 beds in retirement homes and 68 000 beds in long-term care units. There is a very long queue to get into such establishments. For psychiatric institutions, there are a total of 6430 beds. The number of health professionals is quite high (Table 2), but they are growing older and demographic problems will arise in the next 10 years. To finance the health-care system, including ambulatory and hospital care, a budget is approved by parliament annually. Ten percent of the gross domestic product (GDP) is devoted to the health-care system (130bn euros), including public hospitals, private hospitals, ambulatory care organizations and pharmacies (Table 3). The budget is being constantly increased. Patients can get a refund of the total cost of health care. For example, refunds for hospitalization costs are between 80% and 100%. For ambulatory care, refunds are between 70% and 100% and for drugs, between 35% and 100%. Health care is free for the homeless and poor people (100% refund). There is a list of 30 severe diseases, including Alzheimer's disease (AD), for which patients are entitled to a 100% refund. Last year, the treatment of AD was listed as a national priority and the government established a care program for the disease. Two main initiatives were proposed. The first one is diagnosis, particularly early diagnosis, as only half of the patients are diagnosed in France. In regard to this, the program proposed the development of memory clinics and regional expert centers. The second initiative is to provide better care for people with AD. This covers ethical issues, the possibility of family caregivers benefiting from some help, financial aid, and the creation of social day-care centers. Hospital care for people with AD is totally paid for by the social security system. Various options are available: short-stay units, rehabilitation units, and day hospitals (of which there are too few) for diagnosis and rehabilitation. Furthermore, people with AD are generally not very welcome in traditional short-stay and rehabilitation units, and it is very difficult to get them a place in such units. Memory clinics are being developed and regional expert centers will be created next year to assist in the early diagnosis of the disease. An expert center must meet specific defined criteria. It must have a multidisciplinary team (neurologists, geriatricians, psychiatrists, and neuropsychologists) and a day hospital for disease diagnosis (capable of handling at least 100 new patients a year). It must also be a source of expertise in research, possess postgraduate knowledge about dementia, and be the centre of a network including general practitioners, ambulatory neurologists and memory clinics of the first degree. Ambulatory care for people with AD is provided by neurologists and psychiatrists (both in insufficient numbers), and by general practitioners, who are not accurately trained for dementia care. Very few geriatricians are included in ambulatory care. Nurses, orthophonists, and physiotherapists are also involved, but again, they are insufficient in number. In other words, social day-care centers should be developed. Social support for patients is financed by a new prestation, the ‘APA’ (personalized prestation for the promotion of autonomy). This prestation was defined in 2002. The amount of the prestation is calculated according to the loss of autonomy. Patients are classified into six groups upon evaluation of their autonomy. It is possible for patients to buy the time of professional social workers and caregivers. The highest level of financial aid they can obtain is 1200 euros per month. Today, 50% of patients are being looked after only by family caregivers. Nursing homes are currently evolving in France. Retirement homes and long-term care units now belong to a single category. The total living expenses comprise three parts: food and housing costs are borne by the patients (through family or social aid); nursing costs are covered by the APA prestation and patients (or their families); and the total cost of medical care is covered by social security (100%). In conclusion, the French health-care system is quite unique since it involves both etatic and liberal organizations. It is an excellent system for patients because of low medical costs, but it requires a high cost of maintenance.

Open access
Healthcare Systems and Practices
Health, Medicine and Society
Social Policies and Family
Original source
Jan 1, 2004¡Lecture notes in computer science
85 cites
Adaptively Secure Feldman VSS and Applications to Universally-Composable Threshold Cryptography

Masayuki Abe, Serge Fehr

Abstract. We propose the first distributed discrete-log key generation (DLKG) protocol from scratch which is adaptively-secure in the nonerasure model, and at the same time completely avoids the use of interactive zero-knowledge proofs. As a consequence, the protocol can be proven secure in a universally-composable (UC) like framework which prohibits rewinding. We prove the security in what we call the singleinconsistent-player UC model, which guarantees arbitrary composition as long as all protocols are executed by the same players. As an application, we propose a fully UC threshold Schnorr signature scheme. Our results are based on a new adaptively-secure Feldman VSS scheme. Although adaptive security was already addressed by Feldman in the original paper, the scheme requires secure communication, secure erasure, and either a linear number of rounds or digital signatures to resolve disputes. Our scheme overcomes all of these shortcomings, but on the other hand requires some restriction on the corruption behavior of the adversary, which however disappears in some applications including our new DLKG protocol. We also propose several new adaptively-secure protocols, which may find other applications, like a sender non-committing encryption scheme, a distributed trapdoor-key generation protocol for Pedersen’s commitment scheme, or distributed-verifier proofs for proving relations among commitments or even any NP relations in general. 1

Open access
2 source records
Cryptography and Data Security
Advanced Authentication Protocols Security
Security in Wireless Sensor Networks
Original source
Jan 1, 2004¡Lecture notes in computer science
54 cites
Zero-Knowledge Proofs and String Commitments Withstanding Quantum Attacks

Ivan DamgĂĽrd, Serge Fehr, Louis Salvail

The concept of zero-knowledge (ZK) has become of fundamental importance in cryptography. However, in a setting where entities are modeled by quantum computers, classical arguments for proving ZK fail to hold since, in the quantum setting, the concept of rewinding is not generally applicable. Moreover, known classical techniques that avoid rewinding have various shortcomings in the quantum setting.<br /> <br />We propose new techniques for building <em>quantum</em> zero-knowledge (QZK) protocols, which remain secure even under (active) quantum attacks. We obtain computational QZK proofs and perfect QZK arguments for any NP language in the common reference string model. This is based on a general method converting an important class of classical honest-verifier ZK (HVZK) proofs into QZK proofs. This leads to quite practical protocols if the underlying HVZK proof is efficient. These are the first proof protocols enjoying these properties, in particular the first to achieve perfect QZK.<br /> <br />As part of our construction, we propose a general framework for building unconditionally hiding (trapdoor) string commitment schemes, secure against quantum attacks, as well as concrete instantiations based on specific (believed to be) hard problems. This is of independent interest, as these are the first unconditionally hiding string commitment schemes withstanding quantum attacks.<br /> <br />Finally, we give a partial answer to the question whether QZK is possible in the plain model. We propose a new notion of QZK, <em>non-oblivious verifier</em> QZK, which is strictly stronger than honest-verifier QZK but weaker than full QZK, and we show that this notion can be achieved by means of efficient (quantum) protocols.

Open access
3 source records
Cryptography and Data Security
Blockchain Technology Applications and Security
Cryptographic Implementations and Security
Original source
Aug 1, 2002¡Journal of Pain and Symptom Management
11 cites
Spain

Carlos Centeno, S. Hernansanz, Luis Alberto Flores, Álvaro Sanz Rubiales ¡ 5 authors

Abstract This chapter offers an in-depth look at health politics and the tax-financed, universal health system in Spain. It traces the development of the Spanish healthcare system, focusing in particular on its double transition in the 1980s and 1990s from a centralized social insurance system, mostly funded through workers’ and employers’ contributions, to a decentralized universal model financed by general taxation. The new national health system aimed at covering all residents and transferred healthcare competences to the regions, i.e. the seventeen Autonomous Communities, a process completed in 2001. Key issues include rationalization, harmonization, and territorial equity-building of the decentralized healthcare system; efficiency improvement through the introduction of private management elements; and cost containment to bolster the system’s financial sustainability in the context of growing demand and scarce resources. As the chapter argues, these challenges along with the remarkable changes in the political party system have increased the political salience of healthcare in public debate in the 2010s, but the prospects for developing consensual healthcare policies have worsened, such that structural problems are likely to persist.

Open access
2 source records
Palliative Care and End-of-Life Issues
Ethics and bioethics in healthcare
Health, Medicine and Society
Original source
Jan 1, 2002¡Lecture notes in computer science
23 cites
Non-interactive Distributed-Verifier Proofs and Proving Relations among Commitments

Masayuki Abe, Ronald Cramer, Serge Fehr

Abstract. A commitment multiplication proof, CMP for short, allows a player who is committed to secrets s, s ′ and s ′ ′ = s · s ′ , to prove, without revealing s, s ′ or s ′ ′ , that indeed s ′ ′ = ss ′. CMP is an important building block for secure general multi-party computation as well as threshold cryptography. In the standard cryptographic model, a CMP is typically done interactively using zero-knowledge protocols. In the random oracle model it can be done non-interactively by removing interaction using the Fiat-Shamir heuristic. An alternative non-interactive solution in the distributed setting, where at most a certain fraction of the verifiers are malicious, was presented in [1] for Pedersen’s discrete log based commitment scheme. This CMP essentially consists ofa few invocations ofPedersen’s verifiable secret sharing scheme (VSS) and is secure in the standard model. In the first part ofthis paper, we improve that CMP by arguing that a building block used in its construction in fact already constitutes a CMP. This not only leads to a simplified exposition, but also saves on the required number ofinvocations ofPedersen’s VSS. Next we show how to construct non-interactive proofs of partial knowledge [8] in this distributed setting. This allows for instance to prove non-interactively the knowledge of ℓ out of m given secrets, without revealing which ones. We also show how to construct efficient non-interactive zero-knowledge proofs for circuit satisfiability in the distributed setting. In the second part, we investigate generalizations to other homomorphic commitment schemes, and show that on the negative side, Pedersen’s VSS cannot be generalized to arbitrary (black-box) homomorphic commitment schemes, while on the positive side, commitment schemes based on q-one-way-group-homomorphism [7], which cover wide range ofcurrently used schemes, suffice. 1

Open access
2 source records
Cryptography and Data Security
Complexity and Algorithms in Graphs
Privacy-Preserving Technologies in Data
Original source
Jan 1, 2001¡Lecture notes in computer science
297 cites
Robust Non-interactive Zero Knowledge

Alfredo De Santis, Giovanni Di Crescenzo, Rafail Ostrovsky, Giuseppe Persiano ¡ 5 authors

. Non-Interactive Zero Knowledge (NIZK), introduced by Blum, Feldman, and Micali in 1988, is a fundamental cryptographic primitive which has attracted considerable attention in the last decade and has been used throughout modern cryptography in several essential ways. For example, NIZK plays a central role in building provably secure public-key cryptosystems based on general complexity-theoretic assumptions that achieve security against chosen ciphertext attacks. In essence, in a multi-party setting, given a fixed common random string of polynomial size which is visible to all parties, NIZK allows an arbitrary polynomial number of Provers to send messages to polynomially many Verifiers, where each message constitutes an NIZK proof for an arbitrary polynomial-size NP statement. In this paper, we take a closer look at NIZK in the multi-party setting. First, we consider non-malleable NIZK, and generalizing and substantially strengthening the results of Sahai, we give the first construction of NIZK which remains non-malleable after polynomially-many NIZK proofs. Second, we turn to the definition of standard NIZK itself, and propose a strengthening of it. In particular, one of the concerns in the technical definition of NIZK (as well as non-malleable NIZK) is that the so-called "simulator" of the Zero-Knowledge property is allowed to pick a different "common random string" from the one that Provers must actually use to prove NIZK statements in real executions. In this paper, we propose a new definition for NIZK that eliminates this shortcoming, and where Provers and the simulator use the same common random string. Furthermore, we show that both standard and non-malleable NIZK (as well as NIZK Proofs of Knowledge) can be constructed achieving this stronger definition. We call...

2 source records
Cryptography and Data Security
Complexity and Algorithms in Graphs
Privacy-Preserving Technologies in Data
Original source
Jan 1, 2000¡Lecture notes in computer science
97 cites
Optimistic Fair Secure Computation

Christian Cachin, Jan Camenisch

No abstract is available for this record.

Open access
2 source records
Cryptography and Data Security
Privacy-Preserving Technologies in Data
Complexity and Algorithms in Graphs
Original source
Jan 1, 2000¡Lecture notes in computer science
79 cites
A Cryptographic Solution to a Game Theoretic Problem

Yevgeniy Dodis, Shai Halevi, Tal Rabin

Abstract. In this work we use cryptography to solve a game-theoretic problem which arises naturally in the area of two party strategic games. The standard game-theoretic solution concept for such games is that of an equilibrium, which is a pair of “self-enforcing ” strategies making each player’s strategy an optimal response to the other player’s strategy. It is known that for many games the expected equilibrium payoffs can be much higher when a trusted third party (a “mediator”) assists the players in choosing their moves (correlated equilibria), than when each player has to choose its move on its own (Nash equilibria). It is natural to ask whether there exists a mechanism that eliminates the need for the mediator yet allows the players to maintain the high payoffs offered by mediator-assisted strategies. We answer this question affirmatively provided the players are computationally bounded and can have free communication (so-called “cheap talk”) prior to playing the game. The main building block of our solution is an efficient cryptographic protocol to the following Correlated Element Selection problem, which is of independent interest. Both Alice and Bob know a list of pairs (a1, b1)... (an, bn) (possibly with repetitions), and they want to pick a random index i such that Alice learns only ai and Bob learns only bi. Our solution to this problem has constant number of rounds, negligible error probability, and uses only very simple zero-knowledge proofs. We then show how to incorporate our cryptographic protocol back into a game-theoretic setting, which highlights some interesting parallels between cryptographic protocols and extensive form games. 1

2 source records
Cryptography and Data Security
Blockchain Technology Applications and Security
Chaos-based Image/Signal Encryption
Original source
Jan 1, 1999¡OpenGrey (Institut de l'Information Scientifique et Technique)
1 cites
On the formulae-as-types correspondence for classical logic

Charles Stewart

The Curry–Howard correspondence states the equivalence between the constructions implicit in intuitionistic logic and those described in the simplytyped lambda-calculus. It is an insight of great importance in theoretical computer science, and is fundamental in modern approaches to constructive type theory. The possibility of a similar formulae-as-types correspondence for classical logic looks to be a seminal development in this area, but whilst promising results have been achieved, there does not appear to be much agreement of what is at stake in claiming that such a correspondence exists. Consequently much work in this area suffers from several weaknesses; in particular the status of the new rules needed to describe the distinctively classical inferences is unclear. We show how to situate the formulae-as-types correspondence within the proof-theoretic account of logical semantics arising from the work of Michael Dummett andDag Prawitz, and demonstrate that the admissibility of Prawitz’s inversion principle, which we argue should be strengthened, is essential to the good behaviour of intuitionistic logic. By regarding the rules which determine the deductive strength of classical logic as structural rules, as opposed to the logical rules associated with specific logical connectives, we extend Prawitz’s inversion principle to classical propositional logic, formulated in a theory of Parigot’s lambda-mu calculus with eta expansions. We then provide a classical analogue of a subsystem of Martin-Lof’s type theory corresponding to Peano Arithmetic and show its soundness, appealing to an extension of Tait’s reducibility method. Our treatment is the first treatment of induction in classical arithmetic that truly falls under the aegis of the formulae-as-types correspondence, as it is the first that is consistent with the intensional reading of propositional equality.

Hermeneutics and Narrative Identity
Aging, Elder Care, and Social Issues
Health, Medicine and Society
Original source