scholarly journals An Interpretation of the Fan Theorem in Type Theory

1998 ◽  
Vol 5 (39) ◽  
Author(s):  
Daniel Fridlender
Keyword(s):  
Type Theory ◽  
Formal Proof ◽  
Final Version ◽  
Fan Theorem

<p>This article presents a formulation of the fan theorem in<br />Martin-L¨of's type theory. Starting from one of the standard versions of the fan theorem we gradually introduce reformulations leading to a final version which is easy to interpret in type theory. Finally we describe a formal proof of that final version of the fan theorem.</p><p>Keywords: type theory, fan theorem, inductive bar.</p>

Type Theory and Formal Proof

2009 ◽  
Author(s):  
Rob Nederpelt ◽  
Herman Geuvers
Keyword(s):  
Type Theory ◽  
Formal Proof

scholarly journals Some Lambda Calculus and Type Theory Formalized

1997 ◽  
Vol 4 (51) ◽  
Author(s):  
James McKinna ◽  
Robert Pollack
Keyword(s):  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Type Systems ◽  
Formal Proof ◽  
Type Checking ◽  
Formal Development ◽  
Formal Definitions ◽  
Pure Type Systems ◽  
System F

"This paper is about our hobby." That is the first sentence of [MP93], the first report on our formal development of lambda calculus and type theory, written in autumn 1992. We have continued to pursue this hobby on and off ever since, and have developed a substantial body of formal knowledge, including Church-Rosser and standardization<br />theorems for beta reduction, and the basic theory of<br />Pure Type Systems (PTS) leading to the strengthening theorem and type checking algorithms for PTS. Some of this work is reported in [MP93, vBJMP94, Pol94b, Pol95]. In the present paper we survey this work, including some new proofs, and point out what we feel has been learned about the general issues of formalizing mathematics. On the technical side, we describe an abstract, and simplified, proof of standardization for beta reduction, not previously published, that does<br />not mention redex positions or residuals. On the general issues, we emphasize the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts. The LEGO Proof Development System [LP92] was used to check the work in an implementation of the Extended Calculus of Constructions<br />(ECC) with inductive types [Luo94]. LEGO is a refinement style<br />proof checker, publicly available by ftp and WWW, with a User's Manual [LP92] and a large collection of examples. Section 1.3 contains information on accessing the formal development described in this paper. Other interesting examples formalized in LEGO include program specification and data refinement [Luo91], strong normalization of System F [Alt93], synthetic domain theory [Reu95, Reu96], and operational semantics for imperative programs [Sch97].

Eliminating dependent pattern matching without K

2016 ◽  
Vol 26 ◽  
Author(s):  
JESPER COCKX ◽  
DOMINIQUE DEVRIESE ◽  
FRANK PIESSENS
Keyword(s):  
Pattern Matching ◽  
Homotopy Type ◽  
Type Theory ◽  
Case Analysis ◽  
Formal Proof ◽  
Functional Languages ◽  
Homotopy Type Theory ◽  
New Type ◽  
New Criterion ◽  
Typed Languages

AbstractDependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general, it is incompatible with new type theories such as homotopy type theory (HoTT). As a consequence, proofs in such theories are typically harder to write and to understand. The source of this incompatibility is the reliance of dependent pattern matching on the so-called K axiom – also known as the uniqueness of identity proofs – which is inadmissible in HoTT. In this paper, we propose a new criterion for dependent pattern matching without K, and prove it correct by a translation to eliminators in the style of Goguen et al. (2006 Algebra, Meaning, and Computation). Our criterion is both less restrictive than existing proposals, and solves a previously undetected problem in the old criterion offered by Agda. It has been implemented in Agda and is the first to be supported by a formal proof. Thus, it brings the benefits of dependent pattern matching to contexts where we cannot assume K, such as HoTT.

Final version of APA Climate Change report released

2010 ◽  
Author(s):  
Howard S. Kurtzman ◽  
Nicolle Singer
Keyword(s):  
Climate Change ◽  
Final Version

Computational Models for Multilayered Composite Shells with Application to Tires

1996 ◽  
Vol 24 (1) ◽  
pp. 11-38 ◽  
Author(s):  
G. M. Kulikov
Keyword(s):  
Type Theory ◽  
Computational Models ◽  
Geometrical Nonlinearity ◽  
Higher Order ◽  
Stress Strain ◽  
Strain Fields ◽  
First Order ◽  
Timoshenko Type ◽  
Joint Influence ◽  
Discrete Layer

Abstract This paper focuses on four tire computational models based on two-dimensional shear deformation theories, namely, the first-order Timoshenko-type theory, the higher-order Timoshenko-type theory, the first-order discrete-layer theory, and the higher-order discrete-layer theory. The joint influence of anisotropy, geometrical nonlinearity, and laminated material response on the tire stress-strain fields is examined. The comparative analysis of stresses and strains of the cord-rubber tire on the basis of these four shell computational models is given. Results show that neglecting the effect of anisotropy leads to an incorrect description of the stress-strain fields even in bias-ply tires.

UTAUT2-Based Questionnaire: Translation to Canadian French, Cross-Cultural Adaptation and Cognitive Debriefing (Preprint)

2020 ◽  
Author(s):  
Isabelle Pagé ◽  
Marianne Roos ◽  
Olivier Collin ◽  
Sean Dean Lynch ◽  
Marie-Eve Lamontagne ◽  
...  
Keyword(s):  
Technology Acceptance ◽  
Research Team ◽  
Real Life ◽  
Cognitive Debriefing ◽  
French Canadian ◽  
Final Version ◽  
French Version ◽  
Canadian French ◽  
Forward Translation ◽  
Consumer Perspective

BACKGROUND From the early stages of development of a new tool or device to its implementation in real-life settings, it is crucial to take the perception of potential users into consideration. A number of theories have been proposed to better understand acceptance of technology. The Unified Theory of Acceptance and Use of Technology (UTAUT) combines eight of these theories and has been shown to accurately predict technology acceptance. An extended version, the UTAUT2, was proposed in 2012 and includes three new concepts to accurately analyze acceptance and usage of technology from a consumer perspective. No validated Canadian French version of this tool currently exists. OBJECTIVE The main objective was to cross-culturally adapt the UTAUT2-based questionnaire for use in the French-Canadian population. A cognitive debriefing involving potential users (workers) and experts (rehabilitation clinicians) was included to confirm clarity and relevance of questionnaire content. METHODS The procedure was developed in line with published guidelines and included five steps: (1) Forward translation by two bilingual members of the research team, (2) Synthesis of the translated versions by the research team, (3) Backward translation by two other bilingual members, (4) Synthesis by a multidisciplinary committee and proposal of the Pre-final Canadian French UTAUT2-based questionnaire, and (5) Cognitive debriefing. Cognitive debriefing consisted in the assessment of the clarity of the pre-final version content by a French-Canadian sample of potential responders (i.e. workers) and by an expert panel of rehabilitation professionals. Experts also appraised the relevance of each item of the pre-final version. Any questionnaire content or item not reaching an 80% inter-rater agreement for clarity or relevance was re-evaluated by the multidisciplinary committee until a final version was unanimously approved. RESULTS The multidisciplinary committee (n=6) was composed of researchers and clinicians from four different backgrounds. Twelve workers and 12 experts participated in the cognitive debriefing step. Each content or item (n=40) was judged as "clear" by at least 92% of the worker sample. When clarity was assessed by the experts, six terms/phrases did not reach 80% agreement and were therefore reviewed by the multidisciplinary committee. Four of the 27 items were also reviewed by the committee following the experts’ relevance assessment. The final version of the Canadian French UTAUT2-based questionnaire was approved unanimously by the members of the multidisciplinary committee. CONCLUSIONS The final version of the Canadian French version of the UTAUT2-based questionnaire is culturally appropriate for use in French-speaking Canada. Further studies are necessary to determine its psychometric properties.

Sign in / Sign up

Export Citation Format

Share Document