text:
Phoebis sennae

Phoebis sennae, the cloudless sulphur, is a mid-sized butterfly in the family Pieridae found in the Americas. There are several similar species such as the yellow angled-sulphur (Anteos maerula), which has angled wings, statira sulphur (Aphrissa statira), and other sulphurs, which are much smaller. The species name comes from the genus Senna to which many of the larval host plants belong.

Distribution
Their range is wide, from South America to southern Canada, in particular southwestern Ontario. They are most common from Argentina to southern Texas, Georgia, and Florida, but are often visitors outside this range becoming more rare further north.

Habitat
The common habitats of this butterfly are open spaces, gardens, glades, seashores, and watercourses.

Diet
The adult butterfly feeds on nectar from many different flowers with long tubes including cordia, bougainvillea, cardinal flower, hibiscus, lantana, and wild morning glory. The larvae also feed on sennas and partridge peas.

Senna hebecarpa (American senna) is a larval host and nectar source for the cloudless sulphur butterfly in the Eastern United States.

Life cycle
The breeding season is dependent on the climate of the area, from midsummer to fall in the cooler areas, to year-round where the climate is warmer.

Egg
The cloudless sulphur starts off as a pitcher-shaped white egg. Eventually it will turn to a pale orange. The egg stage lasts six days.

Caterpillar
Once the egg hatches, a caterpillar emerges that is yellow to greenish, striped on sides, with black dots in rows across the back. The host plant may be sensitive peas (Chamaecrista), sennas (Senna), clovers (Trifolium), or other legumes (Fabaceae). The caterpillar will usually grow to a length between 41 and 45 mm.

Chrysalis
The caterpillar will form a chrysalis that is pointed at both ends and humped in the middle. The chrysalis will be either yellow or green with pink or green stripes. From the chrysalis comes a medium-sized butterfly (55 - 70 mm) with fairly elongated but not angled wings.

Adult
The male butterfly is clear yellow above and yellow or mottled with reddish brown below and the female is lemon yellow to golden or white on both surfaces, with varying amounts of black spotting along the margin and a black open square or star on the bottom forewing. Wing spans range from 4.8 to 6.5 cm (approximately 1.9

to 2.6 in).

Subspecies
Listed alphabetically:
 * P. s. amphitrite (Feisthamel, 1839) – Chile
 * P. s. sennae or P. s. eubule – Jamaica, South Carolina, Kansas, Virginia, Florida, Cuba

Former subspecies

 * P. s. marcellina (Cramer, [1779]) – Mexico, Uruguay, Galapagos, Suriname, Honduras, Brazil, Argentina, Bolivia, Peru - elevated to full species status as Phoebis marcellina in 2020

title: Phoebis sennae


text:
Christchurch Mansion

Christchurch Mansion is a substantial Tudor brick mansion house built in Ipswich, Suffolk, England, by Edmund Withypoll (also written "Withipoll") around 1548–50. The Grade I listed building is located within Christchurch Park and sits by the southern gates close to the town centre of Ipswich. The mansion belonged to various noble families throughout its history but was purchased by the Ipswich Borough Council in 1884. Since 1885, the building has been used as a museum and is today run by the municipally run Colchester and Ipswich Museums Service (CIMS)organisation. The museum's rooms are preserved as past inhabitants would have known them, complete with original items such as furniture, fine clothing and children's toys. The museum also holds a collection of paintings by renowned local artists including John Constable and Thomas Gainsborough. The Mansion is free to enter and booking is not required.

History

Christchurch Park was originally the grounds of the Priory of the Holy Trinity, with an area of many square miles, coming up to the medieval town walls. During Henry VIII's Dissolution of the Monasteries, the monastery was dissolved and the land was purchased by Paul Withypoll, Master Merchant Taylor and Merchant Adventurer, who died in 1547. Upon the manor, known as Christ Church Withipoll, his son and heir Edmund Withypoll built Withipoll House in 1548–50, the ground floor masonry of which remains, although refurbished internally under subsequent owners. A survival from the original is the house's Latin motto, on a stone dated 1549:"'Frugalitatem sic servas, ut dissipationem non incurras.'" His granddaughter Elizabeth Withypoll married Leicester Devereux, 6th Viscount Hereford and the mansion passed to the Devereux family, who rebuilt the upper floors after a fire in about 1670, when the main porch was also added. In 1734, Claude Fonnereau purchased the mansion from Price Devereux, 10th Viscount Hereford. A street next to the park is named after the family.

W.C. Fonnereau in 1848 laid out and developed Fonnereau Road as a superior residential area. In 1894 the mansion was bought by Felix Cobbold from a syndicate of property developments, to save the building from demolition. Cobbold, a wealthy local businessman and philanthropist, then offered to give it to the Ipswich Corporation to establish a Museum and Art Gallery, together with a further £20,000 (equivalent to £0 in ) in Ipswich Stock for the purchase of artworks. His offer was on condition that the Corporation buy the surrounding parkland for the people of Ipswich. It took Cobbold three attempts to get the corporation to agree to this, but in February 1895 the mansion was transferred to the town and in April 1895 the Corporation purchased the central part of the park. The corporation acquired the Upper Arboretum (laid out for public use in 1848) in 1928. Felix Cobbold, among other members of the wealthy Cobbold family, have donated a great deal of land to the people of Ipswich, including the former Ipswich Racecourse.

The restoration of the Mansion for its public opening was the work of the Ipswich architect John Shewell Corder, and its redevelopment as a Museum was undertaken by Frank Woolnough, Curator of the Ipswich Corporation Museum 1893–1920. Woolnough, an active member of the Museums Association and of the Savage Club, also developed its use as a venue for annual meetings of various Societies, and for educational purposes. During this time it was also the home of the archaeological galleries of Miss Nina Layard, over which she had honorary curatorship. Under curator Guy Maynard (1920–1952) the enlargement of the fine and decorative art and furniture collections continued. The Thomas Gainsborough Bicentenary Exhibition of 1927, including also works by George Frost and John Constable, showcased the mansion as the home of a collection of national importance. The structure was further enlarged with the addition of the new Wolsey Art Gallery at the rear, and an entire two-storey wing rescued in 1924 from the demolition of a Tudor merchant's house.

In 2019, the museum hosted Made in Suffolk, an exclusive exhibition dedicated to the Suffolk global superstar Ed Sheeran. It featured many personal items of Ed Sheeran throughout his journey to stardom, including personal sketches, written song lyrics, school reports and famed awards trophies from the Brit Awards and Grammys.

In 2021, three costumes from Marvel Studios' Black Panther were displayed as part of the Power of Stories exhibition. The outfits of T’Challa, Shuri and Okoye featured in the ground-breaking film were displayed alongside Marvel comics, historic museum objects and local stories. The exhibition won a Temporary Exhibition of the Year award at the Museum and Heritage Awards.

Notable works

 * Lady Drury's Closet
 * Golding Constable's Flower Garden and Golding Constable's Kitchen Garden
 * A collection of seventy-seven pastels by Blanche Georgiana Vulliamy of First World War searchlights

Media appearance

 * It was the location for two episodes of BBC One's Antiques Roadshow filmed in 2020 and transmitted in January and March 2021.

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

title: Christchurch Mansion


text:
Anglican Church of Korea

The Anglican Church of Korea (or Episcopal Church of Korea) is the province of the Anglican Communion in North and South Korea. Founded in 1889, it has over 120 parish and mission churches with a total membership of roughly 65,000 people.

Birth of the Anglican Church of Korea
The birth of the Anglican Church of Korea can be traced back to November 1, 1889, when Bishop Charles John Corfe was ordained at Westminster Abbey and inaugurated as the first diocesan bishop of Joseon (Korea). With his colleagues who had been invited to join the mission, he arrived in Incheon Port on 29 September 1890. Nae-dong Anglican Church which is the first Anglican Church in Korea was established by him and Eli Barr Landis (1865–1898) on Sep. 30, 1891 at Nae-dong, Jung-gu, Incheon. He initiated his work in the Seoul area, including Gyeonggi and Chungcheong provinces. He first opened a number of educational institutions, medical facilities and social work centers across the country, such as the Sinmyeong (Faith and Enlightenment) schools and the hospitals in the vicinities of Incheon, Yeoju and Jincheon as well as the orphanages in Suwon and Anjung. The Anglican missionaries also sought possible ways for the church to be integrated into Korean culture. As a result of that effort, there are several Anglican Church buildings which were constructed in the traditional Korean architecture and which survive today such as those on Ganghwa Island. In addition, the early missionaries made pioneering contributions to Korean studies.

Early missionary work
Beginning in 1923 mission work was actively carried out in the northern part of the peninsula such as Pyongan and Hwanghae Provinces. To train the local clergy St. Michael's Theological Institute, the former institution of the present Sungkonghoe University, was established in 1923, followed by the Society of the Holy Cross (convent) in 1925. Also, the cathedral Church of St. Mary the Virgin and St. Nicholas in downtown Seoul was initially constructed in 1924 and is now well known for its unique Romanesque architecture as it is the only one in this fashion in the orient, together with its mosaic murals.

Japanese colonial rule
Due to considerable difficulties with the language barrier, personal health problems, and other incidents, the mission work had little success throughout the later years, especially during the 36-year period of the Japanese colonial rule. This colonial rule caused significant obstacles to Church development in Korea, primarily because those missionaries appeared to have an indifferent attitude to the Korean independence movement at that time.

First native bishop
Despite such an unfavorable situation as illustrated, the first native Korean bishop, Cheon-hwan Lee, was ordained in 1965 after 20 years had lapsed since liberation from Japanese rule. Thus the original Korean mission diocese was formed into the two dioceses of Seoul and Daejeon, followed by the separate additional forming of the Diocese of Busan in 1974. In 1974, he received an honorary CBE from Queen Elizabeth II. He died on 26 March 2010.

Recent expansion
Since the 1970s the Anglican Church has increasingly expanded through opening a number of new churches across country. St Peter's School was founded in 1975 to provide special needs children with effective special education as needed. St. Michael's Theological Seminary was also upgraded to be accredited by the government in 1982 and 10 years later it was again formally upgraded and expanded as a university to satisfies the peoples' great needs in the coming new era.

The three dioceses continued steady growth in numbers of churches and social evangelization under the auspices of the second and third generations of Korean bishops. The Church has thus been active in constructing new church buildings, along with its continued efforts in opening the new additional churches since the mid-1980s. In this context the Board of Mission and Education has played a timely role in offering education and training programs.

On occasion of its centennial anniversary on September 29, 1990, the Anglican Church of Korea reaffirmed its intent under the theme. "Jesus Christ, Life of the Nation", to continue proclaiming the message of life to the people and expediting the peaceful reunification of Korea as desired.

The Provincial Constitution of the Anglican Church of Korea was declared on September 29, 1992, and the first Korean primate was inaugurated on April 16, 1993. Thus, the Church finally has become an independent national church.

Theology
The Anglican Church of Korea has clergy and members reflecting diverse views. The church ordains women as priests and has been doing so since 2001. Regarding issues of human sexuality, some clergy, congregations, and members of the denomination have been affirming and supportive of LGBT rights including by participating in Pride events. The Anglican Church in Korea is considered to be more open toward homosexuality and is openly discussing the matter. One cleric, representing the Anglican Church in a Korean Christian dialogue, presented a "let's see" approach regarding homosexuality.

Structure and leadership
The church was previously under the authority of the archbishop of Canterbury. To mark independence in 1993, the archbishop of Canterbury handed his authority as metropolitan and primate to the first archbishop of Korea. The church now forms a single metropolitical province, consisting of three dioceses: Seoul, Busan, and Daejeon. The primacy rotates between the three; thus the current bishop of Seoul is also the Archbishop of Korea and Primate of the Church.

Archbishops of Korea

 * 1993 – 1995: Simon Kim Seong-su, Bishop of Seoul
 * 1995: Paul Yun Hwan, Bishop of Daejeon(acting archbishop)
 * 1995 – 1997: Benedict Kim Jae-heon, Bishop of Busan
 * 1997 – 2000: Matthew Chung Chul-beom, Bishop of Seoul

Primate of Korea

 * 2000 – 2003: Paul Yun Hwan, Bishop of Daejeon
 * 2003 – 2005: Matthew Chung Chul-beom, Bishop of Seoul
 * 2005: Joseph Lee Dae-yong, Bishop of Busan
 * 2005 – 2006: Andrew Shin Hyeon-sam, Bishop of Daejeon
 * 2006 – 2009: Francis Park Kyeong-jo, Bishop of Seoul
 * 2009: Solomon Yun Jong-mo, Bishop of Busan(acting Primate)
 * 2009 – 2010: Solomon Yun Jong-mo, Bishop of Busan
 * 2010 – 2017: Paul Kim Keun-sang, Bishop of Seoul
 * 2017 – 2018: Onesimus Park Dong-shin, Bishop of Busan
 * 2018 – 2020: Moses Yoo Nak-jun, Bishop of Daejeon
 * 2020 – present: Peter Lee Kyongho, Bishop of Seoul

Diocese of Seoul
The current Diocese of Seoul was founded as the Joseon (Korea) diocese, covering all the Korean peninsula, in 1889. It was split in 1965, to create Taejon diocese, at which point it became Seoul diocese. The current bishop is Peter Kyongho Lee, who has also been Primate since 2020.

Bishops in Korea
The Bishop in Korea was an Anglican missionary appointment from 1889 to 1965 when the diocese was divided.

Bishops of Seoul

 * 1965–1985: Paul Lee Cheon-hwan (Paul Lee, first native bishop; consecrated shortly before 13 August 1965)
 * 1985–1995: Simon Kim Seong-su
 * 1995–2005: Matthew Chung Chul-beom
 * 2005–2009: Francis Park Kyeong-jo
 * 2009–2017: Paul Kim Keun-sang
 * 2017–present: Peter Kyongho Lee

Assistant bishops

 * 1926–1930: Hugh Embling, Assistant Bishop in Corea. Deaconed Advent (19 December) 1909 and priested Advent (18 December) 1910, by Arthur Winnington-Ingram (London) at St Paul's; consecrated Michaelmas (29 September) 1926, by Randall Davidson (Canterbury) at Westminster Abbey.
 * 1951–1963: Arthur Chadwell, Assistant Bishop (Acting diocesan bishop, 1951–1953; deaconed 11 June 1922 and priested 27 May 1923 by Cyril Garbett (Southwark) at Southwark Cathedral; consecrated 30 November 1951 by Geoffrey Fisher (Canterbury) at Westminster Abbey)

Diocese of Daejeon
The Diocese of Daejeon is the Anglican Church in that part of South Korea that includes North and South Chungcheong Provinces; North and South Cholla Provinces and South Kangwon. It was erected from the Joseon diocese in 1965 and split in 1974 to erect Busan diocese.

Bishops of Daejeon

 * 1965–1968: John Daly
 * 1968–1974: Richard Rutt (assistant bishop since 1966)
 * 1974–1987: Mark Pae Du-hwan
 * 1987–2003: Paul Yun Hwan (cons. 14 Oct 1987, by Robert Runcie (Cantuar.) at Hannam University)
 * 2003–2007: Andrew Shin Hyeon-sam
 * 2007–2013: Michael Kwon Hee-yeon
 * 2014-: Moses Yoo Nak-jun

Diocese of Busan
Busan diocese was erected from the Diocese of Daejeon in 1974.

Bishops of Busan

 * 1974–1987: William Choi Chul-hee (cons. 1 June 1974 by Paul Lee (Seoul) at Seoul Anglican Cathedral)
 * 1987–1997: Benedict Kim Jae-heon
 * 1994–2000: Joseph Lee Dae-yong
 * 2000–2011: Solomon Yun Jong-mo
 * 2012–: Onesimus Park Dong-shin

Archives
Archive materials of the Anglican Church's Korean Mission are held at the Cadbury Research Library, University of Birmingham. These include records from 1889 to 1987.

title: Anglican Church of Korea


text:
Talk:Curry–Howard correspondence

Curry-Howard-Lambek
I have removed the term "Curry-Howard-Lambek" from the article as well as some weasel words "Some people refer to the Curry-Howard-Lambek" correspondence. The only place I am able to find the term Curry-Howard-Lambek is the nlab article on "computational trinitarianism" which makes some dramatic and sensational claims about how higher category theory, proof theory and programming language theory are but three perspectives on a single fundamental unifying phenomenon relating computation, logic and space. The hyperbolic language raises red flags for me as I think that it looks bad when Wikipedia articles are uncritical of sensationalist rhetoric. A second problem is that categorical treatments of type theory generally do not capture either beta reduction of programming languages or cut elimination in logics which are both central to the Curry-Howard correspondence. — Preceding unsigned comment added by 100.11.110.225 (talk) 02:41, 13 October 2023 (UTC)

An Error
In the section Curry-Howard-Lambek correspondence there's a remark at the very end:

"Now, there exists $$t$$ such that $$t:\!\!-~ \alpha_1 \times \ldots \times \alpha_n \vdash \beta$$ iff $$\alpha_1, \ldots, \alpha_n \vdash \beta $$ is provable in implicational intuitionistic logic,."

No citation is offered. This is incorrect -- to see why, just notice that $$\alpha_1 \times \alpha_2 \vdash \alpha_1 \times \alpha_2$$ is true in a CCC but its not true that $$\alpha_1 ,\alpha_2 \vdash \alpha_1 \times \alpha_2$$ in implicational intuitionistic logic. The latter sentence is not even grammatical in implicational intuitionistic logic.

The relationship to intuitionistic logic is complicated; the logic provided corresponds to the fragment of intuitionistic logic with $$\top$$ and $$\wedge$$, but not $$\bot$$ and $$\vee$$. Full intuitionistic logic corresponds to a calculus similar to the one presented, but for bicartesian categories. I know this from folklore among logicians and independent research. I will work on a citation. -- Negacthulhu 10:04, 5 July 2010 (UTC) —Preceding unsigned comment added by 207.224.51.38 (talk)

A Second Version
I've felt for some time that this article doesn't give a good introduction to the general reader of what the C-H isomorphism is really about. I had started writing an article about the C-H isomorphism when this article was put up. I haven't had an opportunity to finish mine, but perhaps someone would like to take it and use it, perhaps to supplement the article that is here now.

I've placed my partial draft at Curry-Howard isomorphism/Alt. Please consider my version of that article to have been released under the terms of the GNU FDL. I would be delighted if someone would complete it. -- Dominus 17:47, 13 May 2004 (UTC)

I've put this all in; basically it is there now topped-and-tailed with general discussion. Possibly some of the discussion of styles of intuitionistic proof could in time be moved to appropriate logic articles.

Charles Matthews 08:25, 14 May 2004 (UTC)

Again, we have a switch between C <-> B. Changing

DefLog 05:34, 18 May 2004 (UTC)

Yes, I seem to have gotten them mixed up some time in the distant past. At least my confusion is consistent. Thanks for all the corrections. -- Dominus 14:13, 18 May 2004 (UTC)

To Dos & Name change
I've taken these items from the main body: they shouldn't be public:

 * Proof normalization
 * Pierce's law as call-with-current-continuation cf. continuation
 * Sequent calculus
 * Product and union types analogous to and and or
 * Exception types analogous to false

Also, I've charged in and moved the article from ...isomorphism to ...correspondence: it's my impression the latter is more common in the scientific literature, and it avoids the resulting sillinesses that arise when talking informally about an isomorphism. Charles Stewart 18:29, 25 Aug 2004 (UTC)

 * My impression was the opposite, and google finds five times as many hits for "isomorphism" as "correspondence". -- Dominus 21:50, 25 Aug 2004 (UTC)

 * I didn't try that. Since a lot of these are Wikipedia mirros, it's not quite an unbiased test: I added the token "site:citeseer.ist.psu.edu" to the search and got 60 for correspondence and 167 for iso, which is a ratio of about 2.8.   Do you think the change should be reversed?  I'm running against the Wikipedia popularity policy here, but talking of correspondence rather than iso does relieve some tortured phrases.  Charles Stewart 22:41, 25 Aug 2004 (UTC)

 * Well in a very precise sense it is an isomorphism and therefore all the more remarkable. I've just run across this article and found it really doesn't express the most important part of the isomorphism (that it functions at the level of reductions as well). It needs considerable work. Francis Davey 22:24, 4 Dec 2004 (UTC)

Well, hello Francis. Charles Matthews 23:22, 4 Dec 2004 (UTC)

Hello to you. I mostly post legal articles (having become a lawyer) but I still amuse myself by thinking about logic and programs in my "spare" time. I am sorry to be slightly critical of the article, but it seems to me that one ought to start by explaining the straightforward correspondance between natural deduction normalisation and beta reduction of simply typed lambda calculus (and the other levels of proofs, types etc). Then one can descibe (1) ways of expanding the correspondence; and (2) links with other systems. At the moment we have sequent calculus and not natural deduction, but the isomorphism between cut-elimination and normalisation is itself hard. Francis Davey 15:58, 7 Dec 2004 (UTC)

 * The ideal WP article on this may be a way off. It should be a survey, initially, and certainly no more prescriptive than typical usage is (for example the Hilbert system business is not my approach, but I have seen in print someone saying it was a revelation etc.). I see there is now a compositionality article, which ought to be a help - but probably isn't right now. I like 'compilation' and Kolmogorov (i.e. that what CH does is to nail down some heuristics about solutions to problems in full gory syntactic detail). I used to think that 'compiler verification' was going to explain why we needed this (Chalst is going to think this all very naive, and others too, no doubt ...) until I realised that no one ever verifies compilers anyway. It's not hard to work out that four people looking at the article have come up with four perspectives; so this is time to knuckle down to some classic wiki editing that deals even-handedly withe everything that gets raised. Charles Matthews 17:14, 7 Dec 2004 (UTC)

The naming problem
I've got a long past with this topic, so much so that I probably can't be objective about certain details: my doctorate was on the so-called classical Curry-Howard correspondence and begins with a rant about the misleading way the topic is made use of in many works in the field. While the centre of the topic was Bill Howard's 1969 manuscript, which indeed presented an isomorphism between two formal systems, there are reasons to prefer not to call the topic the Curry-Howard isomorphism, and these are some of mine: As a last point, if I am convinced that 'Curry-Howard isomorphism' is the more widely used term, the people whose judgement I respect most mostly prefer 'formulae-as-types correspondence'; and at the risk of sounding elitist, I think we should prefer the better term even when it is less popular. My preference for this page are: with the latter only under sufferance; also note that the phrase 'Curry-Howard' is disrespectful to those logicians who contributed fundamental insights; I would particularly single out William Tait in this respect. Charles Stewart 02:26, 7 Dec 2004 (UTC)
 * Howard's manuscript was called The formulae-as-types notion of construction, the terminology formulae-as-types correspondence is closest to the source;
 * The topic does not consist in the first place of showing an isomosophism, rather it consists of establishing first an intuitive observation of a correlation between certain notions of construction in type theory, and certain patterns of inference in logic; the presentation of an isomorphism is rather a virtuoso flourish that adds force to this observation. To insist on talk of isomorphism obscures the most important part, which is the intuitive and I think necessarily informal part;
 * There are many important aspects of the theory that cannot be put into isomorphism, because what would have to be regarded as the logical counterpart of the type theoretic construction makes no logical sense: the clearest development of this problem is in Zhaohui Luo's Computation and Reasoning, where he discusses the problems applying the formulae-as-types correspondence to the Extended Calculus of Constructions (essentially one cannot mix dependent sum with System F like polymorphism and expect the result to be entirely logic-like);
 * There's something artificial about Howard's isomorphism: while the simply-typed lambda calculus is a calculus of an obviously fundamental nature, there's something forced about the logical end, namely the idea of labelling assumptions and implies elimination rules. The labels are needed for the isomorphism to work, but before the work of Curry and Howard, no-one working with natural deduction thought to keep track of these; instead the assumption was simply that all assumptions matching the implies elimination rule are discharged.
 * 1) Formulae-as-types correspondence;
 * 2) Curry-Howard correspondence;
 * 3) Curry-Howard isomorphism;

 * My own impression, that there isn't an 'official' isomorphism, is reinforced rather than otherwise by all that. We could of course just call the page 'Curry-Howard' and have done. And the history should be on the page. Charles Matthews 08:30, 7 Dec 2004 (UTC)

 * Certainly it should have a history section, and as noted above the rewriting aspect is weak. To draw out the properly logical dimension of the rewriting aspect depends on making some account of Prawitz's inversion principle, which is a long put-off task for me.  As for the name, what about just formulae-as-types?  That actually occurs as a substring of Howard's manuscript title. Charles Stewart 11:16, 7 Dec 2004 (UTC)

 * We're a bit constrained by the principle that the title should be the common name. (Cf. recent hassles with Hausdorff dimension - it is well established here that the article title is not the place to deal with correct attribution.) I don't really like formulae-as-types; I once put it to Martin Hyland that the proofs-as-programs level was more perspicuous, and he said it was much better. Anyway I would prefer C-H in the title, just because that's how the computer scientists habitually refer to it. Charles Matthews 11:53, 7 Dec 2004 (UTC)

 * In any case, I don't think your suggestion changes anything for the worse, and since it splits the difference between isomorphism/correspondence I guess applying the move is a good thing. If there are no objections, I'll apply the change tomorrow  Charles Stewart 12:45, 7 Dec 2004 (UTC)

Inhabitation not clear
Is the statement that there is no proof of (α → α) → β related to some particular restricted version of lambda calculus? It should probably be explained better why there is no proof. It seems weird. As far as I know, the usual lambda calculus is Touring equivalent, and you can definitely write a program that receives a function of type α → α and returns an arbitrary value of some other type. -- Jirka6

 * There is no proof of (α → α) → β. (And a good thing, since this sentence is false.)  I'm not sure why you think Turing-equivalence is relevant.  If you think that a lambda-calculus program can be written that has type (α → α) → β, perhaps you should try to write one and present it here.  -- Dominus 18:09, 11 March 2007 (UTC)

 * I am no expert on lambda calculus (that's why I am reading this :). Since there is no error, the section should probably be a little bit clearer so that novices like me have an easier time. Are there some implicit limitations on the lambda calculus in question? I was bringing up the Turing equivalence, because I can definitely write a program for TM, or equivalently in Java or Haskell, that does that. For example, the following simple function does exist and has the type (α → α) → β:

 * fnc :: (int -> int) -> String

 * fnc f = "abc"

 * So apparently I am missing something.--Jirka6 01:23, 12 March 2007 (UTC)

 * That function does not have type (α → α) → β; it has type (int → int) → String. Actually its most general type is α → String, but that is not what you were looking for, right? -- Dominus 02:12, 12 March 2007 (UTC)

 * Are α and β some distinguished types? According to section Types, α and β are type variables, so when I set α = int and β = String, the typing of the function fnc corresponds to (α → α) → β. Anyway, how about if I write (using explicit typing) λxα → α . c where c is a constant of type β. Such function accepts objects of type α → α and returns an object of type β, so it should have type (α → α) → β --Jirka6 04:45, 12 March 2007 (UTC)

 * The type of fnc is not (α → α) → β, any more than the type of (λx → x+1) is (α → α); rather, it is (int → int). You seem to know Haskell, so you should know that the type (α → α) is not the same as the type (int → int).  As for your constant of type β, there is no such constant. (We seem to be back to where we started: if you really think there is such a constant, can you exhibit one?) -- Dominus 04:58, 12 March 2007 (UTC)

 * I'm not trying to be unhelpful, but I'm not sure yet where your difficulty lies. Have you tried reading Type inference?  Have you tried giving expressions to your Haskell interpreter and then asking it what types they have?  -- Dominus 04:58, 12 March 2007 (UTC)

 * Thanks. I think that from your comment about the constant I got one thing. The section talks in the main article talks about a pure system without any non-logical axioms. Right? It is probably obvious, but maybe it should be stated explicitly. Moreover, I thought there are three possibilities: (i) a formula is a theorem - it is provable from axioms (one can find a term of that type); (ii) a formula is a contradiction, and (iii) the third possibility you cannot prove the formula is correct, but you can add some axiom that will enable to prove that formula without making the system inconsistent. Based on the wording of the section, I thought (α → α) → β is case (ii), which sounds weird, but it is just case (iii).

 * Re (λx → x+1) isn't of type (α → α) - I thought α just stands for an arbitrary type, that's why I asked if it is some distinguished type (I know that say Ty2 has only two types). —The preceding unsigned comment was added by Jirka6 (talk • contribs) 15:05, 12 March 2007 (UTC).

 * No, it's case (iii) that holds. If (α → α) → β were a theorem of logic, then the system would be inconsistent, and absolutely anything would be provable.  (α → α) is a theorem, so β would follow by modus ponens, and then by substitution, you have anything you want.

 * In the programs-as-types side of the isomorphism, if you had a function `f` of type (α → α) → β, then you could get absolutely any type you wanted out, by calculating something like (f (λx → x)). But that makes no sense, because there is no such function f that would do that.

 * α really stands for stands for the type ∀α.α. Int is an instance of ∀α.α, but not vice versa.  Similarly (int → int) is an instance of ∀α.(α → α), but not vice versa.

 * There is a function of type ∀α.(α → α), and there is a function of type ∀α.(α → Int), and this latter function also is an instance of a function of type ∀αβ.((α → β) → Int). But there is no function of type ∀αβ.(α → α) → β, which is what you were asking about in the first place.

 * I don't know if this helps much. I'm hoping to understand where your confusion lies, so that we can fix up the article, if that is warranted. -- Dominus 18:13, 12 March 2007 (UTC)

 * Thanks a lot for the clarification.

 * First, regarding universally quantified types: First I was not sure what you mean by that because as far as I know, simply typed calculus is not polymorphic. However, should I think of the quantification as meta-quantification? In other words, when searching for terms of α → α, should I see α → α not as a particular type with α being a base type, but instead as a type schema "schema"? And search for an untyped term that could be assigned all types consistent with that schema? (I think this view was inaccessible for me since I was thinking in terms of Church's explicit typing). IF this is true, it seems logical since in propositional logic, by claiming "α → α is a theorem" one means that it is true for any α (even though prop. logic also does not have quantifiers). I think this should be made explicit, because the first sentence of the section talks about λ-expression with any given type without mentioning universal quantification or any schemata.

 * Second, Based on this discussion, I would suggest the following changes to the section:
 * add closed to the first occurrence of lambda-expression with explanation in parenthesis (I know it is in the next para, but it is easy to overlook - I did overlook it).
 * stress that we are talking about a purely logical system without any non-logical axioms, in other words there are no (non-logical) constants.
 * replace the ξ in the typing of the first mentioned function with α. Otherwise, the reader might wonder if there is some reason for using ξ's in this place but α's in the next paragraphs.
 * clarification about the universally quantified types
 * Jirka6 00:44, 13 March 2007 (UTC)

Proposal for revising the article
I'd like to propose a significant revision of the article. Stricto sensu, the Curry-Howard correspondance is the observation in Curry and Feys's book that typed combinatory logic coincided with the axioms for implication in Hilbert-Bernays logic, and the observation by Howard that the proofs of Gentzen's natural deduction could be seen as the terms of a typed lambda-calculus. In my opinion, the article should then be primarily built around these two observations and I would rather suggest the following structure:
 * Introduction
 * Minimal Hilbert-style logic and typed combinatory logic
 * A table for the correspondence
 * Some examples (such as the ones in current section Programs are proofs)
 * Minimal Natural deduction and simply-typed lambda-calculus
 * A table for the correspondence,
 * Some examples
 * Other aspects of the correspondence
 * Other connectives (and, or, quantifiers, absurd type)
 * Classical logic
 * Sequent calculus
 * Discussion
 * Other contributions to the correspondence: use of lambda-notation in Automath
 * Related works: realisability, BHK interpretation
 * Socio-mathematical stimulus: Martin-Löf type theory, Pure Type Sytems, linear logic, category theory
 * "Philosophical" or cultural issues: proving is the same as programming, validating a formula is the same as exhibiting an inhabitant in a type, ...

Especially, I would suggest I don't know what to suggest with the section Point of view of category theory. Did it provide some insights on the proofs-as-programs correspondence before Curry and Howard did (in which case it would typically go to section related works) or has it rather to be seen as a domain which benefited from the correspondence to investigate new topics (in which case it would typically go to section socio-mathematical stimulus). Hugo Herbelin (talk) 20:14, 18 December 2007 (UTC)
 * to remove the section Types of which the contents is already present in page Simply typed lambda calculus,
 * to move the contents of section The type inhabitation problem to the page Type inhabitation problem,
 * to remove the section Intuitionistic logic: its contents is mainly in page Intuitionistic logic,
 * to insert the section Programs are proofs in proposed section Minimal Hilbert-style logic and typed combinatory logic,
 * to rename the section Natural deduction in proposed section Minimal Natural deduction and simply-typed lambda-calculus,
 * to move the sections Classical logic and Sequent calculus as subsections in proposed section Extensions

 * I think that all sounds superb, and I hope you go ahead with your plan and see it through to completion. My suggestion about the Point of view of category theory section would be to delete it.  Ever since it was put in it has always seemed to me that it was more like "point of view of the one person who put it in". -- Dominus (talk) 14:38, 19 December 2007 (UTC)

 * I agree. At its narrowest (the combinatory logic / Hilbert system and the minimal logic / ND equivalence) can be constructed so that the word "isomorphism" is useful in context. That is less true the further away from these you move (eg the correspondence between sequent calculi and natural deduction systems is very subtle and not straightforward at all). Francis Davey (talk) 18:04, 19 December 2007 (UTC)

 * Yes, when moving from Hilbert system (and its correspondence with combinatory logic) and from ND (and its correspondence with typed lambda calculus) to sequent calculus, there is no longer an exact correspondence (in the sense of a matching of structures) between sequent calculus and a pre-existing notion of computation. However this is an active field of research to find such an appealing computational counterpart to sequent calculus and some progresses have already been made. Being personally involved in this field of research, I would however advance only with precaution to avoid any risk of undue subjectivity. 62.212.105.93 (talk) 17:04, 24 December 2007 (UTC)

 * Interesting, who are you and what are you doing? I spent a lot of time trying to use graphs (i.e. interaction nets/proof nets to do just this but resources are difficult). Really the problem with sequents is that they have a lot of bookkeeping information that is uninteresting logically and computationally so one wants to factor it out. Francis Davey (talk) 17:56, 24 December 2007 (UTC)

 * I'm a researcher in proof theory, lambda-calculus, etc. The extra bookkeeping information in sequent calculus (if I understand correctly what you mean by bookkeeping information) can be explained by the "fact" that sequent calculus has the potentiality to interpret both a call-by-name and a call-by-value lambda-calculus while ordinary natural deduction only contains a call-by-name lambda-calculus. More precisely, classical sequent calculus contains two dual subsystems called LKT and LKQ that respectively correspond (in the sense of the Curry-Howard correspondence) to a call-by-name and a call-by-value lambda-calculus. Hugo Herbelin (talk) 21:27, 24 December 2007 (UTC)

 * Finally I did not find anything really relevant to the Type inhabitation problem page in the Type inhabitation problem. The section had examples of inhabited and non inhabited types/propositions that were relevant for the current article but, for inhabitation, it was I, K and S which are already mentioned in the article, while for non inhabitation there were no convincing explanation of why they were non inhabited so I renounce to do anything with the examples. I deleted the section and the only reference to inhabitation is now in the main table of correspondences.
 * The section Point of view of category theory is very difficult to evaluate. It could not understand the relation between Curry-Howard and "compilation" mentioned in the section. Can the author or somebody else explain? Paragraph 3 was just general ideas about BHK interpretation and CCC and I did not see the link with Curry-Howard. Paragraph 4 suggested that Lambek contributed to the proof-as-program and formula-as-type correspondence. I followed the suggestion of Dominus and removed the section Point of view of category theory but I added in the related works section a subsection on the so-called Curry-Howard-Lambek correspondence that is referred to in some papers. Hugo Herbelin (talk) 21:29, 24 December 2007 (UTC)

I completed my process of revision. There are still many things to say and to improve but I believe I now have a consistent article and I stop here. I hope to have correctly preserved the significant informations that were present in the version of 21 December 2007 before I started the revision. I'm not fully satisfied by the typography of formulas and inference rules. I find the <math> environment not very elegant. I would have prefered to move everything to unicode but I have been told that some can't see symbols like ⊢ (the same using math mode: $$\vdash$$) in IE on Windows (by the way, a few of these unicode ⊢ are still in the article). Hugo Herbelin (talk) 17:48, 28 December 2007 (UTC)

 * Thanks very much. I printed it out a couple of days ago and was reading it over this morning.  It is very clear and coherent, and I think it is a big improvement on what went before.

 * I marked up my printout with minor corrections to grammar and wording, and I will put these changes in when the opportunity arises.

 * Thanks again for your work on this article. -- Dominus (talk) 20:56, 28 December 2007 (UTC)

Article name
I moved from an en-dash that was in the article title, which is very unusual, to a hyphen as is used throughout it. Why was the en-dash in there, anyone know?

Now, I see above that there have been arguments about whether to name this "Curry-Howard isomorphism" or "Curry-Howard correspondence" -- but is "Curry-Howard" alone superior to either of those? Unless anyone has a good reason not to, I would like to have this moved back to "Curry-Howard isomorphism" (of the two, that gets by far the most google hits.) MilesAgain (talk) 12:32, 29 December 2007 (UTC)

 * I agree. -- Dominus (talk) 15:09, 29 December 2007 (UTC)

 * There were already a discussion about this question and I agree with Charles Stewart that it is more common to use the word correspondence in the scientific community than to use the word isomorphism. I think that the reason is double:

 * Curry-Howard is an isomorphism. But Curry-Howard is more than an isomorphism as it says that proofs and typed programs are identical. Otherwise said, if we care about formalizing them properly, we would define them exactly the same way. Hence, from the mathematical point of view, saying that Curry-Howard is an isomorphism is the same as saying that a square is a rectangle. A square is a rectangle, but you lose information when you say that a square is a rectangle.
 * At the beginning, Curry-Howard was a surprising and unexpected result. For logicians, proofs and programs were really thought as different at that time, and that's why, I think, the correspondence has been often thought as an isomorphism, i.e. as the property that two different kinds of objects had the same structure (but they are not different!).

 * Now that Curry-Howard is widely accepted and that logicians design calculi that are both proof systems and programming languages, it makes more sense IMHO to call it a correspondence rather than an isomorphism.

 * Then, if correspondence is, I think, better than, say identity (which would still be mathematically accurate), it is because even if they are mathematically the same, they are not exactly the same in the way we think about it. For proofs, the meaningful part is the proved formula while for typed programs, the meaningful part is the program. And more generally, there are still two distinct vocabulary.

 * Coming back to the primary question, whether the page should be called Curry-Howard or Curry-Howard correspondence, I have no serious opinion. The full name is a bit long to type in so I would prefer the short form but the long form is (again IMHO) more precise and could be preferable too.

 * I know that, even if I give arguments to lay my point of view, there is still a part of subjectivity in it, and I would be interesting to hear arguments in the other direction. Hugo Herbelin (talk) 18:38, 29 December 2007 (UTC)

 * You have convinced me that "Curry-Howard correspondence" is the right choice, but "Curry-Howard" alone is terrible because it's just a pair of names, not a noun phrase. Please understand that there will always be a redirect from Curry-Howard to this article, just as Curry-Howard correspondence redirects here now. I requested "Curry-Howard correspondence" at WP:RM. MilesAgain (talk) 05:04, 30 December 2007 (UTC)

Relationship with logic programming
The basic idea of logic programming is that axioms are programs and proofs are program executions, i.e. computations. As far as I know, there has been no correspondence shown between these different ideas.Logperson (talk) 12:39, 26 February 2008 (UTC)

 * Of course, as you already (or probably should) know: the relations between the two fall under the header of the Automath project and all other endeavors related to or inspired by it. So, your request is really an implicit request to include a link in the main article to Automath. — Preceding unsigned comment added by 129.89.251.51 (talk) 21:49, 7 October 2011 (UTC)

Who is the audience?
I'm having a pretty hard time reading this article. I have only a vague idea of what intuitionistic logic is, I don't know what "Hilbert-style" logic is, and I only know what "the empty type" and "the singleton type" are from the discussion later in the article that explains that they are bottom and unit, which I have vague ideas about from ⓐ trying to read papers on formal logic and ⓑ using OCaml.

 * The simplest remedy for this is to simply link everything up to Intuitionistic_logic, Heyting_algebra, Complete_heyting_algebra (which is the same thing as a "locale", which in turn is the type of lattice the Open_sets of a Topological_space form; also see Birkhoff's_representation_theorem, Pointless_toplogy and Stone_duality), Typed_lambda_calculus, Categorical_abstract_machine, Category_theory, Categorical_logic, Topos, Proof_theory, Sequent_calculus, Natural_deduction and Gentzen. There's never a reason, opportunity (or excuse) to say "I don't know" when you're in the middle of the an Encyclopedia(!)

But I know what the lambda-calculus is, I have some experience programming in OCaml, and I've proved simple theorems in first-order predicate logic textbook exercises, although I don't know which first-order predicate logic. Last year I wrote a λ-calculus interpreter that works by reducing λ-expressions to combinator graphs (although I had forgotten this was called "abstraction elimination") and then performing combinator-graph reduction to evaluate them.

So I have the idea, perhaps unreasonable, that I ought to be able to read an article introducing the Curry-Howard isomorphism. A friend of mine explained some of the basics to me some years ago: that you can write functions with type α × β → α, or α × β → β, or α → β → α, or α → β → β, or α × (α → β) → β, but not functions of type, say, α → β, because then what would type β be? Nor can you write a function of type α × (β → α) → β, because that function doesn't have any way to come up with any particular value of type β; all it has is an input that could transform some value of type β to a value of type α, if you had a β to start with. And that this corresponds pretty much exactly to the

But the article doesn't seem to be written with people like me in mind. It assumes a lot of background knowledge that I don't have, and without which I am unable to make much sense of the article. I have tried to read papers on the application of symbolic logic to programming occasionally for ten years now, without success.

On the perhaps vain hope that this is merely an oversight, rather than that the article is intended for people who already know a lot about symbolic logic, I am listing the things that I wish were explained in the article:

 * What are "product types" (tuple types?), "sum types" (discriminated unions?), "the empty type" (an empty set, i.e. the absence of a result for programs that crash or hang?) and "the singleton type"?
 * What are "dependent product" and "dependent sum"?
 * Are the formulas "α → (β → α)" and "(α → (β → γ)) → ((α → β) → (α → γ))" the only possible axiom schemes? ("schemas"?)
 * Is "Γ₁, α, Γ₂ ⊢ α" supposed to be parsed as "(Γ₁, α, Γ₂) ⊢ α" or as "Γ₁, α, (Γ₂ ⊢ α)"? Do the commas mean "and"?  If so, why are there two Γs?
 * In the table of inference rules, I am guessing that the things above the line are the sufficient conditions from which we can derive the things below the line? But I thought the things on the left side of the ⊢ were the sufficient conditions for deriving the thing on the right side of the ⊢?  Are the horizontal line and ⊢ just different notations for the same thing?
 * What does "Γ₁, x : α, Γ₂ ⊢ x : α" mean? I guess the colon indicates that what comes before it is of the type that follows it?  Does this mean that we can deduce that x is of type α, or something else?  Or does it represent that we can compute the value of x itself, given its value?  I have the impression, perhaps false, that even if my other confusions about notation would be obvious to anyone who knew anything about logic, that the meaning of this side of the table is likely to only be comprehensible to someone who already understands the correspondence.
 * I assume the "constructor" under "Programming side" refers to things like Just and Nothing, which construct a value of some type, and not the meaning of "constructor" from C++? What is a "destructor" in that context, just any function that pattern-matches on values of such a type?
 * In the example of proving α → α, in the first step, where do the formulas α, β → α, and α come from? They clearly aren't the types of S, K, and K.

I am restricting my complaints to sections that I feel I would have some hope of understanding if the notation and vocabulary were explained. Perhaps placing some examples earlier in the article, before explaining the general principles, would help too.

If there is another article that explains this stuff, or if it is felt peripheral to the point of this article, maybe there could be a link early in the article saying, "The symbolic logic notation used in this article is briefly explained in some thousand-word-or-less article explaining the basics of the notation"?

I think that, in general, one of the things that makes an article encyclopedic is that it is accessible to the lay public.

I hope this is helpful, and I am grateful for the work of the article's many editors over the years in attempting to bring the Curry-Howard light to us unenlightened peons, even though their work has not been able to penetrate my thick skull.

Kragen Javier Sitaker (talk) 10:54, 22 December 2008 (UTC)

 * I think these are all good criticisms that should be addressed... One quick fix: it might help to read section 4 on natural deduction<->lambda calculus before reading section 3 on Hilbert-style deduction<->combinatory logic. It seems section 4 explains some of the notation used in section 3, such as the list notation for contexts...and in general lambda calculus/ND make a lot more sense than combinatory logic/Hilbert-style deduction ;) Perhaps section 4 was written first, and the order was reversed to reflect the chronological order? From an expository point-of-view, I think it would be best to explain ND<->λ first, since both sides (or at least the right-) are most familiar. Noamz (talk) 08:39, 30 September 2009 (UTC)

Minor question on Origin, scope, and consequences
The second paragraph of the first section ends with, "This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run." This seems like a non sequitur. What is a "form of logic programming" supposed to mean? Functional programming? Noamz (talk) 08:15, 30 September 2009 (UTC)

Church vs Curry in General Formulation
I'm not sure it's a good idea to talk about Church vs Curry and intersection/union types so soon. Currently the article states only that there is a choice of how to interpret the universal and existential quantification, but this applies just as well in the binary case of conjunction and disjunction. So I think it would be better to discuss intersection and union types (both binary & infinitary versions) either in a later section, or perhaps leave them out of the article entirely (because I don't think there is a well-established answer as to what they correspond on the logic side). Noamz (talk) 08:26, 30 September 2009 (UTC)

 * Agreed. I've just read that part of the article for the first time, and I think at best it is confusing, at worst it is wrong.  The links to "intersection types" and "union types" don't help, because they only talk about binary intersections and unions, which is the normal meaning of the term.  It seems that what is meant is intersection (or union) indexed by an element of a type - which seems like a dependent type to me, and that's what I'm used to seeing them called even when they are curry-style.  Church vs curry affects what kinds of expressions are in the language, but it doesn't affect the structure of the types.  I think leaving out this distinction is best unless someone has a good reference for why it's important to make it.  —Preceding unsigned RowanD (talk) 07:33, 19 July 2010 (UTC)

What is the interest in using of The curry-howard correspondence for proof assistant for instance Coq?
Hi, Thank you if you can answer!

I'm living in France and try to learn mathematical logic on french and english wikipedia ,because mathematics fascinate me and I got interested in Automated theorem proving ...The question may appear to be stupid, but I don't understand what does it permit to use such a correspondence in proof assistant? From what I understood, it can be useful for normalisation of deductions ( changing deduction to one which is nicer), but I don't understand how it can permit to more easily prove that a statement is true or false?

I'll be very grateful if you can answer me! Thank you for all of you for having written this page.

--Nicobzz (talk) 16:28, 23 December 2010 (UTC)

 * It means you can have a computer do the proof for you, instead of doing it by hand. It also means that when you have a proof, then you also have an algorithm, and so maybe you can use that algorithm to compute something useful.  You can also automatically search for proofs, using, for example, genetic algorithms. More generally, simply being aware of the correspondence makes it easier to think clearly about what one is actually doing. 99.153.64.179 (talk) 21:24, 26 June 2013 (UTC)

Homotopy type theory
At the risk of making this article longer, there should be some quick review of homotopy type theory which, one could say, is version 2.0 of the ideas here. After reviewing a bunch of basic type-theory articles at WP (e.g. product type, dependent type) its woefully clear that these are lacking as compared to what can be found in e.g. chapter 1 of the HoTT book. The ncatlab website one-ups the HoTT book in these areas, e.g. by not only defining terms but also showing how category theory models some of these ideas from type theory. So, I guess I'm saying that each one of these correspondences could be worked up into a full-fledged article: e.g. how a dependent product type is like an universal quantifier, worked out in detail. This correspondence goes even further: John Baez has an article "Rosetta Stone" which notes that cartesian-closed cats are generalized by symmetric monoidal categorys; that the internal language of CCC's being simply typed lambda calc is similarly generalized by linear logic, and that both of these correspond in turn to cobordisms. (The mind-bender is, of course, that cobordisms underlie string theory, and homotopy underlies K-theory so the connections/equivalences/etc are... fascinating?) So basically, the correspondence described here is broader/deeper/wider than this article lets on, and even the basics here can certainly be articulated in much greater detail. 99.153.64.179 (talk) 21:18, 26 June 2013 (UTC)
 * I just now added a tame version of above to the end of the article. Much work is still needed on many other articles; besides the many different basic type articles, but also these red links: equality type identity type which eventually should lead to univalence axiom, but also more simply judgement (type theory) judgement (logic) judgement (sequent calculus) to discuss the internal/external split of reasoning about logic. And inhabited type  is a redlink.  99.153.64.179 (talk) 22:17, 26 June 2013 (UTC)

Curry-Howard or BHK?
The article gives no references that Curry and Howard first discovered this, and Robert Harper (computer scientist) writes (also without references):
 * Neither Curry nor Howard discovered the principle (Howard himself disclaims credit for it), though they both did make contributions to it. Moreover, this unfortunate name deprives credit to those who did the real work in inventing the concept, including Brouwer, Heyting, Kolmogorov, deBruijn, and Martin-Löf.  (Indeed, it is sometimes called the BHK Correspondence, which is both more accurate and less grandiose.) (from "Extensionality, Intensionality, and Brouwer’s Dictum")

75.15.115.75 (talk) 06:43, 1 August 2013 (UTC)
 * A Google search reveals an Elsevier logic vol 149 Lectures on the Curry-Howard Isomorphism which probably documents reasons for denoting the isomorphism this way. Philip Wadler's notes on The Curry-Howard Isomorphism include Howard's 1980 "The formulae-as-types notion of construction" I am reminded of how Richard Feynman could never quite utter the word "Feynman" in connection with his Feynman Diagrams. He would not vocalize his name in this context. This similarity points to Howard as the originator of the isomorphism, even if Howard never took credit. The community of researchers has already awarded the credit. __Ancheta Wis   (talk  | contribs) 11:31, 1 August 2013 (UTC)
 * On a related note, I've always wondered why we have a separate article on the BHK interpretation. The reference there ( Section 5.5.) does give some additional detail on both their histories. —Ruud 09:09, 1 August 2013 (UTC)

Wadler has documented the history in Propositions as Types:
 * This reading of proofs goes back to the intuitionists, and is often called the BHK interpretation, named for Brouwer, Heyting, and Kolmogorov. Brouwer founded intuitionism, and Heyting and Kolmogorov formalised intuitionistic logic, and developed the interpretation above, in the 1920s and 1930s. Realisability, introduced by Kleene in the 1940s, is based on a similar interpretation.
 * Given the intuitionistic reading of proofs, it hardly seems surprising that intuitionistic natural deduction and lambda calculus should correspond so closely. But recall that Gentzen invented Sequent Calculus because he could not find a direct proof of the Subformula Property for Natural Deduction, and the direct proof was not published until three decades later, by Prawitz. As pointed out to Howard by Martin Löf, Prawitz’s technique for normalising a proof corresponds exactly to reduction of lambda terms. Gentzen, Church, and Prawitz never drew these parallels. Certainly Howard was proud of the connection he drew, citing it as one of the two great achievements of his career [43]. While the connection may be obvious in retrospect, it was far from obvious in prospect!
 * Howard’s paper divides into two halves. The first half explains a correspondence between two well-understood concepts, the propositional connectives &, ∨, ⊃ on the one hand and the computational types ×, +, → on the other hand. The second half extends this analogy, and for well-understood concepts from logic proposes new concepts for types that correspond to them. In particular, Howard proposes that the predicate quantifiers ∀ and ∃ corresponds to new types that we now call dependent types.

His sources include Howard himself Howard on Curry-Howard.

I have tried to format this, because I can not read it, but I gave up
a:β → α, b:γ → β, g:γ ⊢ b : γ → β   a:β → α, b:γ → β, g:γ ⊢ g : γ ——————————————————————————————————— ———————————————————————————————————————————————————————————————————— a:β → α, b:γ → β, g:γ ⊢ a : β → α      a:β → α, b:γ → β, g:γ ⊢ b g : β ————————————————————————————————————————————————————————————————————————               a:β → α, b:γ → β, g:γ ⊢ a (b g) : α ————————————————————————————————————               a:β → α, b:γ → β ⊢ λ g. a (b g) : γ → α ————————————————————————————————————————                        a:β → α ⊢ λ b. λ g. a (b g) : (γ → β) -> γ → α ————————————————————————————————————                                ⊢ λ a. λ b. λ g. a (b g) : (β → α) -> (γ → β) -> γ → α

Started to format with LaTeX, but I failed.

$$ \frac{a:\beta\to\alpha,\ b:\gamma\to\beta,\ g:\gamma \mathop{\ \vdash\ }b:\gamma\to\beta\qquad\qquad a:\beta\to\alpha,\ b:\gamma\to\beta\mathop{\ \vdash\ } g:\gamma}{\frac{a:\beta\to\alpha\mathop{\ \vdash\ }}{\mathop{\ \vdash\ }}} $$

I do not know how to do this without the \infer macro

I also think that Bfgx=f(gx) where x : α, g : α → β, f : β → γ, Bfg : α → γ is more familiar for programmers and those who know Bfg  as f.g

If I failed to fix this, what to say my intent to build commuting diagrams.

maybe someone more skilled than me can make this article more readable  — Preceding unsigned comment added by 2806:107E:4:15E:218:DEFF:FE2B:1215 (talk) 10:32, 27 May 2017 (UTC)

title: Talk:Curry–Howard correspondence


text:
Template talk:POV

Adding a parameter
Hi,

I've added a  parameter to this template in its sandbox, and tested it on the testcases page. I think it would be useful to have the option to display a reason in this template. Of course, this wouldn't be a replacement for discussing things on the talk page, but it could at least provide a short explanation of what the problem is. Does anyone have any comment on this? Regards, DesertPipeline (talk) 13:48, 16 March 2021 (UTC)
 * I wonder whether having the option of using a reason parameter would discourage editors from initiating a Talk page discussion... DonIago (talk) 16:45, 19 March 2021 (UTC)
 * User:Doniago: Well, if they don't initiate a talk page discussion, isn't another person allowed to remove the template? Also I just realised that it could help with that anyway, because if the reason is sufficiently descriptive, someone else who agrees with it could start the discussion rather than simply removing the template. I feel like the only way to know for sure though is to trial it by adding the parameter and seeing how it goes. What do you think? Regards, DesertPipeline (talk) 08:29, 22 March 2021 (UTC)
 * If the editor who adds the template is required to initiate a Talk page discussion, which appears to implicitly be the case (they're not strictly required to do so, but as you note, the tag can be removed if there isn't such a discussion), then I'm not sure whether the reason parameter will really add anything to the situation. Maybe editors who are concerned by the tag should need to read the full discussion (if any) rather than walking away with just the reason provided. I have to admit I'm a little unsympathetic to the case of editors who might apply this tag but not start the implicitly-required discussion; they don't need to start it themselves, but should coordinate with another editor at that point. Adding the parameter may also confuse editors who believe that supplying a reason obviates the need for a discussion. DonIago (talk) 20:50, 23 March 2021 (UTC)
 * User:Doniago: You have fair points. I guess let's see if anyone else has any thoughts on this parameter as well. I do personally think it would be useful, and I proposed it because I have use for such a parameter at the moment, but I get what you mean. Thanks, DesertPipeline (talk) 05:25, 24 March 2021 (UTC)
 * Absolutely! Just expressing my opinions here, and I'm happy to defer to whatever consensus may emerge, and might even rethink my own views depending on what others have to say. Thank you! DonIago (talk) 06:09, 24 March 2021 (UTC)
 * I agree that some users are unlikely to use DonIago. But I like the idea of giving more information. As an alternative what about automatically creating a Talk discussion with the editor name and the comment from the publish if an NPOV is added on an article. If they give no reason, the the discussion has "no reason given. If uncertain please contact editor, or if you can't work out why remove "Wakelamp d[@-@]b (talk) 06:00, 12 November 2021 (UTC)
 * I'd be curious to hear from other editors on this, and see test cases. If your quote is the exact wording you think should appear, then I think it needs refinement as well. DonIago (talk) 19:29, 12 November 2021 (UTC)

Edit request to complete TfD nomination
Template:POV has been listed at Templates for discussion (nomination), but it was protected, so it could not be tagged. Please add:

to the top of the page to complete the nomination. Thank you. –LaundryPizza03 ( d c̄ ) 22:55, 7 November 2021 (UTC)
 * ✅ * Pppery * it has begun... 23:01, 7 November 2021 (UTC)

Edit request to remove TfD tag
The discussion has ended; please remove the TfD tag (that is,  at the top). Thanks, Tol  (talk | contribs) @ 04:52, 10 November 2021 (UTC)
 * ✅ firefly  ( t · c ) 07:43, 10 November 2021 (UTC)

Placement dispute
Hi. I placed this template on the article Conspiracy theory because I believe it is not neutral. User:Beyond My Ken removed it with the rationale, "No support for NPOB tag on talk page". It is my understanding that is not a reason to remove it per this template's guidance.

I reverted indicating Beyond My Ken doesn't WP:OWN the article, but the user reverted again, with the rationale, "The tag should not represent a single editor's viewpoint, it should reflect that a significant percentage of the editors discussing the issue agree that there is a neutrality problem -- that isw most definitely NOT the case here. Do not resore unless you have that". But according to the lead of this template, "Place this template on an article when you have identified a serious issue of balance and the lack of a WP:Neutral point of view, and you wish to attract editors with different viewpoints to the article." It doesn't say I must seek consensus first to add it.

Advice is welcome. Regards, Thinker78  (talk) 06:13, 2 August 2023 (UTC)
 * Tags should not be used to express personal dissatisfaction with an article. Instead, clear reasons for the tag need to be provided on article talk. Documentation does not cover obvious things such as the fact that of course consensus is needed for anything in an article, including a tag. The discussion at Talk:Conspiracy theory does not support your position. By the way, some thought would show that accusing another editor of OWNING an article is not appropriate given that you seem to think you OWN the right to insert a tag. Johnuniq (talk) 07:36, 2 August 2023 (UTC)
 * @Johnuniq I literally followed the guidance of this template, therefore i thought it was inappropriate to remove it and indicated to Beyond My Ken that they don't own the article. I tried following this template's guidance when adding the tag. Beyond My Ken in my opinion did not. Because the template guidance clearly talks in a singular you that places the tag, it doesn't indicate that I must seek consensus to add it because it is actually a tag to seek consensus. Therefore, you appear to have a circular argument. Regards, Thinker78  (talk) 23:17, 2 August 2023 (UTC)
 * I have mixed feelings regarding Johnuniq's response to you, so I'll just say that while technically you aren't required to start a discussion regarding your POV concerns either before or after adding this tag, I think the instructions make it pretty clear that adding the tag without any supporting discussion at the Talk page may result in other editors removing it, similarly without discussion.
 * As such, if you have legitimate concerns about the POV on that article, I would encourage you to start a discussion at the article's Talk page and then add the tag, perhaps after waiting a couple of days to see how other editors feel regarding your concerns. However, if the Talk page discussion that Johnuniq linked to already addresses the neutrality concerns that you intended to highlight, then it would seem that there's already a consensus that the neutrality is not an issue. DonIago (talk) 14:20, 2 August 2023 (UTC)
 * I agree with your explanation, in fact it's obviously correct. No one needs to get permission to edit an article or to add a tag. However, no one needs permission to revert an edit or remove a tag. After that, discussion and consensus is required. Johnuniq (talk) 23:26, 2 August 2023 (UTC)

title: Template talk:POV


text:
Frankie Banali

Francesco Felice Banali (November 14, 1951 – August 20, 2020) was an American rock drummer, most widely known for his work with heavy metal band Quiet Riot. His signature tone and iconic drum intros first became famous on their album Metal Health, which was the first metal album to hit number one on the Billboard charts and ushered in the 80's metal band era. He had been the band's manager since 1993. He had also played the drums in the heavy metal band W.A.S.P., as well as with Billy Idol. Banali was briefly a touring drummer for Faster Pussycat and Steppenwolf. In the last few months of his life, he was also an inclined painter.

Life and career
Banali was born on November 14, 1951, in Queens, New York City, New York, to Italian immigrants, Jack and Martha Banali. In 1975, he moved to Los Angeles, where he spent four years playing drums with various bands, including Steppenwolf with Nick St. Nicholas and Goldy McJohn. He was a very prolific session player and played on many hits for other artists including Billy Idol's "Mony Mony" and "L.A. Woman" and over 100 recordings. He also played drums on the acclaimed "Hughes/Thrall" album with Glenn Hughes and Pat Thrall. In 1979, Banali, along with bassist Dana Strum, was in secret rehearsals with then Quiet Riot guitarist Randy Rhoads and Ozzy Osbourne as the latter was looking for a guitar player to launch a new band. In 1980, he joined forces with Kevin DuBrow and formed DuBrow with a revolving door of musicians, before settling with former Snow guitarist Carlos Cavazo and bassist Chuck Wright. After Rudy Sarzo replaced Wright, DuBrow changed the name of the group to Quiet Riot (which was the same name of the band that DuBrow, Sarzo and Randy Rhoads had used prior to Sarzo and Rhoads leaving to join Ozzy Osbourne's band). After signing with Pasha Records in September 1982, Banali and Quiet Riot found success with Metal Health, which was released six months after signing their deal with Pasha Records. In November 1983, only eight months after its release, Metal Health reached the #1 spot on the Billboard 200 charts (replacing the Police's Synchronicity), making it the first heavy metal album to go #1 on the charts. Metal Health eventually sold over 10 million copies worldwide and help usher in the decade of heavy metal hair rock.

By the time Condition Critical was released in July 1984, tensions began to slowly break Quiet Riot apart, but Banali held on, through lineup changes and a diminishing fan base (mostly caused by Kevin DuBrow's erratic behavior). By 1989, Quiet Riot disbanded after touring in support of their self-titled album, which was released in October 1988. Around the time of recording their self-titled album, he also played drums for W.A.S.P.'s The Headless Children album. After Quiet Riot disbanded, he rejoined W.A.S.P. to tour in support of the album. In 1990, Banali was called in by Faster Pussycat to replace the fired Mark Michals, during their tour in support of their 1989 album Wake Me When It's Over. After his mother's death in November 1990, Banali regrouped and formed a band called Heavy Bones with guitarist Gary Hoey. They released only one album in 1992, before disbanding. In 1993, Banali rejoined Quiet Riot after Bobby Rondinelli left the band to join Black Sabbath. In 1994, he also took over as the band's manager, overseeing the band's business decisions. After three albums and more lineup changes (including the reunion of the classic Metal Health lineup from 1997 onwards), Quiet Riot disbanded in 2003. Banali and DuBrow reformed Quiet Riot in October 2004 with bassist Chuck Wright and new guitarist Alex Grossi. They released one album with the lineup, Rehab in 2006, before the untimely death of DuBrow in November 2007. Banali announced the dissolving of Quiet Riot on January 14, 2008.

It would not be until September 2010 that Banali (with the blessing of Kevin DuBrow's family) reformed Quiet Riot with Wright and Grossi. They originally hired Mark Huff, but he was let go in January 2012. While Keith St. John came in to fulfill the tour dates, they hired Scott Vokoun in March 2012. In November 2013, Vokoun left and was replaced by Jizzy Pearl. And in June 2014, Quiet Riot released 10, their first album in eight years. In mid-2010, Banali had an online fundraiser via Kickstarter with his then fiance Regina Russell Banali for the seed money for production of a documentary about the band, titled Quiet Riot - Well Now You're Here There's No Way Back, a film she both produced and directed. The final amount raised was nearly $24,000, The film premiered at the Newport Beach Film Festival on April 29, 2014.

On January 18, 2017, Frankie was inducted into the Metal Hall of Fame for his contribution to Heavy Metal drums.

Banali was interviewed for the 2020 book, BONZO: 30 Rock Drummers Remember the Legendary John Bonham, by author Greg Prato.

Influences
Frankie Banali's main influences include John Bonham (rock drumming) and Buddy Rich, (traditional Jazz drumming). For standard drumming his influences were Simon Phillips, Dennis Chambers, and Vinnie Colaiuta, just to name a few

Personal life and death
Frankie's father, Jack, died from pancreatic cancer in 1974. Frankie's mother, Martha, died after an eight-year battle with breast cancer, on November 14, 1990, Frankie's 39th birthday.

Frankie married his first wife, Karen (born 1969), in 1994. On February 17, 1997, his daughter, Ashley, was born. On April 14, 2009, Karen died from heart failure at the age of 40.

On November 11, 2015, Frankie married his second wife Regina Russell Banali, who produced and directed a documentary about Quiet Riot called Quiet Riot: Well Now You're Here, There's No Way Back.

In October 2019, Banali revealed that he was diagnosed with stage-IV pancreatic cancer on April 17. He died from the disease on August 20, 2020, at age 68. This left Banali as the second member of the classic Metal Health-era Quiet Riot lineup to have died, following Kevin DuBrow in November 2007. It was announced three weeks after his death that Quiet Riot would continue without Banali, who was replaced by Johnny Kelly.

On September 4, 2020, as a result of a fan-led petition, MTV Classic on their Metal Mayem show, which aired every Friday evening from 9 PM to 1 AM EST, aired a rock block of Quiet Riot videos to honor Frankie. The block started at the beginning of the show and included these 6 videos: "Party all Night", "Twilight Hotel", "The Wild and the Young", "Bang Your Head (Metal Health)", "Mama Weer All Crazee Now", and "Cum On Feel the Noize". At the beginning of each video text in blue and white scrolled in from the right and lasted a few seconds saying "In Memory of Frankie Banali, 1951-2020". The block lasted 37 minutes which included commercials between the third and fourth videos.

Vic Vergeat Band

 * Vic Vergeat Band (1982)

With Hughes/Thrall

 * Hughes/Thrall (1982) (tracks 6 & 9)

With Billy Thorpe

 * East of Eden's Gate (1982)

With Quiet Riot

 * Metal Health (1983)
 * Condition Critical (1984)
 * QR III (1986)
 * QR (1988)
 * Terrified (1993)
 * Down to the Bone (1995)
 * Alive and Well (1999)
 * Guilty Pleasures (2001)
 * Rehab (2006)
 * Quiet Riot 10 (2014)
 * Road Rage (2017)
 * Hollywood Cowboys (2019)

With Hear 'N Aid

 * Hear 'n Aid – "Stars" (1986)

With Kuni

 * Masque (1986)

With Alex Masi

 * Attack of the Neon Shark (1989)

With W.A.S.P

 * The Headless Children (1989)
 * The Crimson Idol (1992)
 * Still Not Black Enough (1995)
 * Unholy Terror (2001)
 * Dying for the World (2002)
 * The Neon God: Part 1 - The Rise (2004)
 * The Neon God: Part 2 – The Demise (2004)
 * Re-Idolized (Soundtrack to the Crimson Idol) (2018)

With Heavy Bones

 * Heavy Bones (1992)

With Blackthorne

 * Afterlife (1993)

With Julliet

 * Passion (2002)

title: Frankie Banali


text:
The Girl Who Was Plugged In

"The Girl Who Was Plugged In" is a science fiction novella by American writer James Tiptree, Jr. It won the Hugo Award for Best Novella in 1974.

Plot summary
The story takes place in a dystopian future where the world is controlled by a capitalist regime. Despite advertising being illegal ("ad" is, in fact, a dirty word), corporations are still able to persuade and control consumers by the celebrities they create for product placement. The protagonist, seventeen-year-old Philadelphia Burke, or P. Burke, is enlisted to become one of these celebrities after a suicide attempt fueled by society ostracizing her due to her Pituitary Dystrophy, better known as Cushing's Disease. While recovering in the hospital, she is chosen by a scout to become a "Remote Operator" for the beautiful corporate creation, known as Delphi, who was grown without a functioning brain from a modified embryo in an artificial womb. Though Delphi appears to be a normal fifteen-year-old-girl, she is controlled through a satellite linked to P. Burke's brain, which is still physically located in her original body.

The Remote and the Operator
The purpose of a remote and a remote operator, such as Delphi and P. Burke, is to remove the fear a company might have that a normal celebrity could act of their own accord. P. Burke controls Delphi, making her say and do whatever the company tells her to. That being said, after months of training, Delphi is strategically placed in a minor documentary film, and she becomes a media sensation overnight. Her job is to act as a celebrity traveling all over the world, all the while subtly buying and promoting products to influence the public in favor of a company.

A Harsh Reality
P. Burke not only falls in love with the life style, but Delphi as well. Acting as a perfect teenage girl, P. Burke has everything she has ever wanted. She has fame, respect, wealth, power, and eventually love. Paul Isham, the rich and rebellious son of a network executive, notices Delphi on the set of her Soap Opera and falls in love with her. P. Burke - and, by default, Delphi - reciprocates his feelings, but cannot let him know the truth. He eventually discovers and misunderstands the situation, believing Delphi is a normal girl who is enslaved by implants. He breaks into the lab where P. Burke is and is shocked to see Delphi being controlled by an unattractive, bedridden woman connected to countless machines. Out of rage and confusion, he rips the wires out of P. Burke, killing her. Delphi remains biologically "alive" and is put under the control of another operator.

Analysis
The underlying discussions that take place in relation to "The Girl Who Was Plugged In" tend to focus on the female body and gender embodiment. In her article titled ""Whatever It Is that She's Since Become": Writing Bodies of Text and Bodies of Women in James Tiptree Jr.'s "The Girl Who Was Plugged In" and William Gibson's "Winter Market"", Heather J. Hicks puts focus on Tiptree's take on female embodiment in the form of P. Burke. Tiptree uses phrases like "pumped-out hulk", "girl brute" and "carcass" to devalue P. Burke, which further increases her feeling of uselessness in the story. This negative version of female embodiment is shown in contrast to the positive embodiment seen through Delphi, who is described as "flawless" and "beautiful". The juxtaposition of these two bodies allows for a discussion on the way different types of bodies function within the context of society presented throughout the story.

Different types of bodies
Two different types of bodies are presented throughout the story. Heather J. Hicks explains that Delphi is the body with value, while P. Burke is seen as the opposite. This obsession with perfection is seen through the use of celebrities, including Delphi, as advertisements. Her beauty gives her influence over the population, which in turn gives her opportunities that P. Burke will never have. Only through the proxy of Delphi can P. Burke be valued in society. Hicks explores this idea further, saying "P. Burke welcomes the chance to shed the ignominious flesh and bone that have caused her so much suffering" in order to become more valued. This means that P. Burke is willing to get rid of her own physical body in order to move up in society because she understands that it will never happen any other way. Social status within this society is so dependent on perfection and beauty that those who do not fall into that category want to move into better bodies. Hicks says this is precisely what gender disembodiment means within the context of "The Girl Who Was Plugged In".

Gender of the author
There is an obvious relationship between the gender of the author and the message of the story. Hicks explains that Tiptree uses P. Burke as a metaphor for herself. The author, whose real name is Alice Bradley Sheldon, uses the male pen name of James Tiptree Jr. in order to be successful in the world of science fiction. Hicks says Sheldon "becomes P. Burke, which powers the public persona that consumers desire". Not only does Sheldon use a male pen name, but her writing style is viewed as masculine as well. This further contributes to the gender embodiment that Tiptree tries to undertake. Like those in the story, consumers in the science fiction world want a body image that represents what they deem worthy. In the story, people want an idealized female body, and in the real world science fiction consumers want a male body producing their stories. Hicks says the way in which P. Burke is ousted by Paul "suggests a conviction that her own body of work would not endure the revelation of her female body". In this method of analyzing the situation, Tiptree is suggesting that by writing this story she cannot be successful as a science fiction writer in her own body. Melissa Stevenson sums up this point in her article "Trying to Plug In: Posthuman Cyborgs and the Search for Connection" by saying that "The Girl Who Was Plugged In" "is a tale of transformations and masks, the story of a girl who is not who she seems to be, written by an author who is not exactly who "he" seemed to be".

A male author for a male audience
One notable characteristic of "The Girl Who Was Plugged In" is how the author used a male narrator to tell the story to a predominantly male audience in order to play with the reader's expectations of how the story will pan out. The story is being told by way of a male narrator most likely to a 1970's male science fiction consumer. The story continuously being told through a male point of view comes to highlight issues that male readers might have when reading this short story. According to Stevenson, Tiptree utilizes this way of telling the story in order to influence male readers expectations of P. Burke and of the ways the story will turn out upside down. The narrator rebukes the reader on several occasions for having these false expectations. Stevenson gives an example of this with the actual attempted suicide of P. Burke on the park bench. The narrator chastises the reader because he is not interested in P. Burke but rather the surrounding city. The expectation here is that the life of the ugly P. Burke is relatively unimportant compared to the surroundings to the targeted male reader. Stevenson points out that after this, the reader is rebuked three different times for not focusing on P. Burke but each time this happens, the narration is moved to descriptions of the futuristic soundings, presumably in accord with what the male reader truly desires to read about. This goes back to what Heather J. Hicks states about the importance and success of the ideal feminine body compared to the non-ideal feminine body. P. Burke’s body is considered unimportant and the way the story is written and paced suggests just that.

The performance of gender
Another theme of "The Girl Who Was Plugged In" is the performance of gender. According to Veronica Hollinger, this story is about P. Burke’s pursuit of the ideal feminine body. P. Burke desperately wants to achieve this ideal body, but she cannot due to her physical appearance. According to Hollinger, P. Burke is performing the gender ideal through a distance by controlling Delphi. Hollinger states that P. Burke’s performance here gives her an opportunity that she would not otherwise have given her real body to “mimic acceptable femininity". She also says that P. Burke “is the divinely feminine Delphi as long as she performs Delphi. P. Burke is the actor and Delphi is her role”. This performance was P. Burke’s way to a fairy-tale ending. Delphi can only be feminine if she were to be performed in a feminine way. Hollinger’s entire analysis can be seen in parallel with the analysis of Heather J. Hicks when she discusses how P. Burke uses Delphi to push herself up in the ranks of society. In order to have more opportunities in the society presented, P. Burke must perform femininity through Delphi.

Literary criticism on the portrayal of the body
The depiction of the body in "The Girl Who Was Plugged In" has been discussed by several feminist literary scholars. Amongst them are Scott Bukatman, Melissa Colleen Stevenson, Veronica Hollinger and Heather J. Hicks. Major themes in "The Girl Who Was Plugged In", as seen in the aforementioned authors articles referenced in this section, include disembodiment and re-embodiment, performance of femininity, oppression of the female body by cultural power structures and the female body in a technological society.

Constructed ideal of femininity
Veronica Hollinger, co-editor of the scholarly journal "Science Fiction Studies" of DePauw University, states in her article, "(Re)reading Queerly: Science Fiction, Feminism, and the Defamiliarization of Gender", that women are forced to conform to a constructed ideal of femininity in order to avoid being seen as a failure or, to some extent, incomplete. To Hollinger, "The Girl Who Was Plugged In" is about the ways women experience pressure from society to fulfill the set standards of femininity as seen in P. Burke's desperate desire to fully leaving her real body and re-embody permanently as Delphi. In a society where the only way to achieve happiness is by conforming completely to a constructed ideal, P. Burke has little choice but to live through the perfect girl body that is Delphi. Heather J. Hicks reinforces Hollinger's views in her article "”Whatever It Is That She’s Since Become”: Writing Bodies of Text and Bodies of Women in James Tiptree, Jr.’s “The Girl Who Was Plugged In” and William Gibson’s “The Winter Market”" by stating that P. Burke denies her unappealing, real body. Hollinger sees P. Burke as a representation of the body that is utterly insignificant in the eyes of society. She discusses "The Girl Who Was Plugged In" in terms of how gender can act as a form of imprisonment when society expects an unrealistic display of femininity ). P. Burke's existence becomes meaningful only when her mind controls the beautiful but "empty" body called Delphi, thus the female body in meeting with technology creates a separation between the body and the mind where P. Burke's only way of fulfilling the feminine beauty ideal is at the hands of technology. The futuristic world in which Tiptree Jr. stages her story has taught P. Burke to idolize the ideal that "the Gods" embody and so P. Burke willingly commits the act of "performing femininity".

Description of P. Burke
Another way disembodiment and oppression of the female body is seen in "The Girl Who was Plugged In" is by the words used to describe the main character, i.e. the description of P. Burke. Early in the story Tiptree says, “That’s good, because now you can see she’s the ugly of the world. A tall monument to pituitary dystrophy. No surgeon would touch her.” In the opinion of Scott Bukatman, of Stanford University, Tiptree forms the body into something unclean and decaying through phrases such as "dead daddy", "rotten girl" and "zombie". Hicks suggests the use of crude words for the main character only gets worse as the story progresses to emphasize an unappealing display of female disembodiment. According to Bukatman, the body in "The Girl Who Was Plugged In" is a dominating and central figure, but it also serves to represent a definite limitation. This relates to Hollingers statement of P. Burke's re-embodiment as Delphi becoming an actor/role relationship where P. Burke imagines herself as an actor that must fulfill a role, i.e. Delphi. This is a clear parallel to our own society's failure to recognize the individual women as separate from the constructed cultural ideal of femininity. Stevenson's view is that, to the deformed and shunned P. Burke, her life as Delphi is the only one that is actually real, because her original body left her excluded from the "human" category in the eyes of society, making her unable to form emotional connections or experience love until her re-embodiment as Delphi. Consequently, P. Burke feels more human as Delphi than as herself because society finally accepts and recognizes her existence. In other words, P. Burke is dependent on technology to be able to participate in society.

Relationships between women and technology
While Hollinger reads "The Girl Who Was Plugged In" through the ideological lens of gender as a performance, Hicks believes Tiptree connects female disembodiment with women's relationship to technology. Delphi, who was made for the sole purpose of advertising, is the living example of the perfect woman, and through her work for GTX she participates in reinforcing the cultural ideal of the femininity she's created after. In Hicks opinion, "Delphi's body is used in a capitalistic aim for the purpose of advertising to such an extent that her body becomes synonym with the products she advertises". However, Stevenson points out that, while Delphi is beautiful, she does not have an identity without the connection to P. Burke, which means they are both dependent on each other in order to function in society. Bukatman also argues that the act of merging with a machine, like P. Burke merges with Delphi, is, in feminist science fiction, an act of defeat, as opposed to the romanticized approach of cyberpunk where it is seen as necessary and a source of power. Bukatman points out that technological advances in science fiction are synonym with the furthering of a patriarchal power structure, as seen in the control of the female body in "The Girl Who Was Plugged In". Bukatman states; "In this sense, Tiptree's title refers to the state of being plugged in to male definitions of the feminine image and being; plugged in to the power structures of male technology.". He also points out the negative impact of altering your identity in Tiptree's story, and states that it serves as a symbol of oppression rather than liberation from society's conventions.

P. Burke and Delphi vs. Sheldon and Tiptree
Stevenson and Hicks both discuss the interesting and noteworthy parallel between P. Burke and Delphi and Alice Sheldon and her pseudonym, James Tiptree Jr. Stevenson points out that by writing under a male pseudonym, Sheldon was able to obtain a more "attractive" exterior with which she could connect to the male dominant science fiction writing community. Hicks believes that Sheldon herself may have experienced a form or disembodiment where she could only fulfill the ideals of the science fiction community by assuming a male persona. By the numerous ways Tiptree has touched on essential feminist topics in a single short story, it becomes clear why she was one of the most prominent feminist science fiction writers of her time.

Publications

 * The Ultimate Cyberpunk. Pat Cadigan. iBooks, 2002. ISBN 0-7434-5239-9
 * New Dimensions 3. ed. Robert Silverberg. Doubleday, 1974.
 * Warm Worlds and Otherwise. Collection of stories by James Tiptree, Jr. Ballantine, 1975.
 * Her Smoke Rose Up Forever. Anthology of stories by James Tiptree, Jr. Tachyon, 2004.
 * The James Tiptree Award Anthology 3, edited by Karen Joy Fowler, Pat Murphy, Debbie Notkin, and Jeffrey D. Smith. Tachyon, 2007.
 * Tor Double #7: "Screwtop". Vonda N. McIntyre. "The Girl Who Was Plugged In". James Tiptree, Jr.. Tor, 1989. ISBN 0-8125-4554-0.

Other media

 * The story was adapted as a television film in 1998, for the Sci Fi Channel series Welcome to Paradox (episode 5).
 * The story was adapted as a stage musical in 1992, as the first act of "Weird Romance: Two One-Act Musicals of Speculative Fiction". Music was by Alan Menken, Lyrics by David Spencer, Book by Alan Brennert and David Spencer. It starred Ellen Greene in its Off-Broadway premiere and the cast recording.

title: The Girl Who Was Plugged In


text:
Rosebuds

Rosebuds may refer to:

 * Adamstown Rosebuds, a football (soccer) club
 * Portland Rosebuds (ice hockey), two professional ice hockey teams based in Portland, Oregon during the 20th century
 * Portland Rosebuds (baseball), a professional baseball team based in Portland, Oregon in 1946
 * The Rosebuds, an indie rock band
 * Victoria Rosebuds, a minor league baseball team

title: Rosebuds