text:
Cord (automobile)

Cord was a brand of American luxury automobile manufactured by the Auburn Automobile Company of Connersville, Indiana, from 1929 to 1932 and again in 1936 and 1937.

Auburn was wholly owned by the Cord Corporation, founded and run by E. L. Cord as a holding company for his many transportation interests (which included the Lycoming engines, Stinson aircraft, and Checker Motors). Cord was noted for its innovative technology and streamlined designs.

Innovations
Cord innovations include front-wheel drive on the L-29 and hidden headlamps on the 810 and 812.

Though DeSoto used them in 1942, hidden headlamps did not reappear as a luxury feature until the 1960s, beginning with the 1963 Chevrolet Corvette. It was followed two years later by another General Motors product, the Buick Riviera, whose GM stylists later stated they were trying to capture the "feel" of the Cord's design.

"Servo" shifting was accomplished through a Bendix electro-vacuum pre-selector mechanism (a type of electromechanical shifting).

Cord L-29
This was the first American front-wheel drive car to be offered to the public, beating the Ruxton automobile by several months, in 1929. The brainchild of former Miller engineer Cornelius Van Ranst, its drive system borrowed from the Indianapolis 500-dominating racers, using the same de Dion layout and inboard brakes. Built in Auburn, Indiana, the Cord was the first front-wheel-drive car to use constant-velocity joints. While commonly used today in all front-wheel-drive vehicles, their first use was on the 1929 Cord. The lack of rear drivetrain components and straight frame (without rear kick-up to clear up the rear axle) allowed it to be much lower in height than competing cars whose average height was about six feet or almost two metres. Both stock cars and special bodies built on the Cord chassis by American and European coachbuilders won prizes in contests worldwide. The L-29 came with full instrumentation, including a temperature gauge, oil pressure gauge, and speedometer on the left with a gas gauge, oil level gauge, and ammeter on the right of the steering wheel.

It was powered by a Lycoming 4934 cc 125 hp L-head inline 8 from the Auburn 120, with the crankshaft pushed out through the front of the block and the flywheel mounted there, driving a three-speed transmission. Gearing in both transmission and front axle was inadequate, and the 4700 lb car was underpowered, limited to a trifle over 80 mph, inadequate even at the time, and readily exceeded by the less expensive Auburn. Still, the styling was lovely, and despite the 137.5 in wheelbase and steering demanding fully four turns lock-to-lock, handling was reportedly superb. Wheelbase was 137.5" and the height of the sedan was 61". The 1930 Chrysler Imperial and Chrysler Eight copied several styling elements.

The L-29 was priced around US$3,000 ($0 in dollars ), putting it in the upper tier of America's most expensive luxury automobiles alongside Cadillac, Marmon, Lincoln, Packard, Franklin, and Stutz, and below only Duesenburg. It could not, however, outrun the Great Depression, and by 1932, it was discontinued, with just 4,400 sold.

Cord Model 810/812

The Model 810/812 are probably the best-known of the company's products. Styled by Gordon M. Buehrig, they featured front-wheel drive and independent front suspension. By placing the transmission ahead of the engine Buehrig was able to eliminate the driveshaft and transmission tunnel. Accentuating its sleek, low-slung look, he also dispensed with running boards. Powered by a 4739 cc Lycoming V8 of the same 125 hp as the L-29's straight-8, the 810 had a four-speed electrically selected semi-automatic transmission,(called a pre-selector because you selected the gear and then stepped on the clutch) among other innovative features like roll up headlights.

The car caused a sensation at the New York Auto Show in November 1935. Orders were taken at the show with Cord promising Christmas delivery, anticipating production of 1,000 per month. Delays pushed hoped delivery to February 1936 - which still proved optimistic, with owners only beginning to get the first cars in April. In all, Cord managed to sell only 1,174 of the new 810 in its first model year. The car's distinctively squared-off front end and pioneering, streamlined, horizontally louvered grille design earned it the durable nickname "coffin nose".

Demise
Early reliability problems, including slipping out of gear and vapor lock, cooled initial enthusiasm, and the dealer base shrank rapidly. Unsold left-over and in-process 1936 810s were re-numbered and sold as 1937 812s. In 1937, Auburn ceased production of the Cord. A single 1938 Cord prototype with some changes to the grille and transmission cover was built, and it still exists (2015). The Cord empire, amid allegations of financial fraud, was sold to the Aviation Corporation, and E.L. Cord moved to Nevada where he earned millions in real estate and other enterprises.

Hupmobile/Graham

In 1940 ailing automakers Hupmobile and Graham-Paige tried to save money and revive the companies, by using the 810/812 body dies. Except for their similarity to the 810, their four-door sedans, the Hupp Skylark and the Graham Hollywood, were unremarkable. Retractable headlights gave way to plain headlight pods, and power came from a standard front-engine/rear-wheel drive design. While Hupp Motor Company built a few prototypes in 1939 that gained them sales orders for the 1939 model year they did not have the resources to manufacture the car. Graham Paige stepped in offering to build the Hupmobile Skylarks on a per piece contract basis. Graham built a combined 1850 units for sale in the 1940 model year. Hupmobile closed before the 1941 model came around. Of the 1850 cars produced in the 1940 model year by Graham only about 450 were the Hupmobile Skylarks. Graham continued to build the Hollywood late into 1941. They stopped production in November of that year having only built a rumored 400 units. The Hollywood was powered by a supercharged Continental in line six making 124 HP, almost 50 less than the original supercharged Cord.

Trivia
The plot of the David Niven movie Where the Spies Are features a rare Cord convertible as the incentive for the hero to undertake an espionage mission. The movie was based on the James Leasor novel Passport to Oblivion, which is one of a series of suspense/intrigue novels featuring the fictitious Dr. Jason Love, whose "infatuation" with the Cord roadster played a prominent part.

In the novel Live and Let Die, Felix Leiter drives a Cord of unspecified model when he and James Bond are in Florida.

The original design for the Batmobile was a red convertible based on the Cord 812, which Batman creator Bob Kane considered one of his favorite vehicles and fitting for the millionaire vigilante.

The 1965 film What's New Pussycat? featured a rather battered red Cord 810 convertible with French selective yellow headlights. The car was piloted in several scenes by Woody Allen whose character drove on the Paris pavements (sidewalks).

A yellow Cord 810 is seen driven by young gangster Bobby Malto in the 1991 TV-Movie "The Return of Eliot Ness", which starred Robert Stack, reprising his title role from "The Untouchables" 1959-1963 TV series.

In the 1994 film The Shadow, Moses Shrevnitz (Peter Boyle) drives a 1936 Cord 810 Westchester that was stretched and custom-painted as a taxi cab.

"bePUZZLED" brand puzzles is a series of puzzles which feature a short mystery story to go along with the picture in the assembled puzzle. A puzzle and story in the series is called A Classic Case of Murder and features a creme colored 1936 810 Cord in the story and pictured in the puzzle. Copyright 1992.

In the 2001 PlayStation exclusive car combat game Twisted Metal: Black. The playable driver No-Face has a car based on the Cord 810, nicknamed "Crazy 8".

In the 2002 PC and PlayStation 2 game Mafia: The City of Lost Heaven the Cord 810 and 812 are featured under a cover-up names Thor 810 and Thor 812 FWD. The Thor 810 is based on the normally aspirated version with no outside exhaust, while the Thor 812 FWD, available only as a convertible in the game, is based on the supercharged version with the outside exhausts on the side of the engine bay. The player could even feel the car being front wheel drive, as the game featured sophisticated physical model of all cars (and guns for that matter) and so the Thor handled differently than the other rear driven cars. In the 2020 remake of the game, only one version is featured under the name Berkeley 810 and is derived from the two door supercharged version with a solid roof.

As part of his series Jay Leno's Garage in 2013, Jay featured his own Cord 812 which he had previously written about in Popular Mechanics. The car had been lovingly restored by amateur restorer Arthur Pirre.

On Gram Parsons' 1973 album GP, the song "The New Soft Shoe" is written about E.L Cord and his famous automobiles.

In classic crime film The Godfather, a Cord 810 convertible is briefly seen on the estate of Jack Woltz.

A 1930 Cord L-29 is featured prominently in HBO's 2011 Mildred Pierce (miniseries).

Some sung versions of Rodgers and Hart song The Lady is a Tramp refer to "Lincolns and Cords"

title: Cord (automobile)


text:
Cord

Cord or CORD may refer to:

Common meanings

 * String
 * Thin rope
 * Twine
 * Cord (climbing) a type of rope used in climbing
 * Cord (unit) used for measuring wood
 * Power cord
 * Umbilical cord

Cord or CORD may also refer to:

Places

 * Cord, Arkansas

People

 * Alex Cord (1933–2021), American actor and writer
 * Chris Cord (born 1940), American racing driver
 * Errett Lobban Cord (1894–1974) American industrialist
 * Ronnie Cord (1943–1986), Brazilian singer
 * Cord McCoy (born 1980), American bull and saddle bronc rider
 * Cord Meyer (1920–2001), American CIA official
 * Cord Parks (born 1986), American professional football player
 * Cord Phelps (born 1987), American professional baseball player
 * Cord Pool, guitarist for American red dirt metal band Texas Hippie Coalition
 * Cord Widderich (died 1447), German pirate

Arts, entertainment, and media

 * Cord (band), a British rock group
 * Cord (film), a 2000 film starring Daryl Hannah and Jennifer Tilly
 * Cordero "Cord" Buchanon, a fictional character in One Life to Live
 * The Cord Weekly, a student newspaper at Wilfrid Laurier University

Biology

 * Chronic obstructive respiratory disease or CORD, an alternate name for chronic obstructive pulmonary disease
 * Mycelial cord, a structure, used by fungi to transfer nutrients over larger distances
 * Spinal cord
 * Umbilical cord, a tube that connects a developing embryo or fetus to its placenta

Organizations
Organizations with the acronym CORD include:
 * Canadian Organization for Rare Disorders, a non-profit health organization
 * Christian Outreach for Relief & Development, a humanitarian organization, based in Leamington Spa, England
 * Coalition for Reforms and Democracy, a Kenyan political coalition
 * Council of Emergency Medicine Residency Directors, a scientific organization

Computing

 * An electrical cable
 * Rope (data structure) or cord, a data structure for strings

Other uses

 * Cord (sewing), a decorative trim made of multiple strands of yarn twisted together
 * Cord, a short form for the textile type corduroy
 * Cord Automobile, a former American car marque

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

title: Cord


text:
Ultramicroscope

An ultramicroscope is a microscope with a system that lights the object in a way that allows viewing of tiny particles via light scattering, and not light reflection or absorption. When the diameter of a particle is below or near the wavelength of visible light (around 500 nanometers), the particle cannot be seen in a light microscope with the usual methods of illumination. The ultra- in ultramicroscope refers to the ability to see objects whose diameter is shorter than the wavelength of visible light, on the model of the ultra- in ultraviolet.

Synopsis
In the system, the particles to be observed are dispersed in a liquid or gas colloid (or less often in a coarser suspension). The colloid is placed in a light-absorbing, dark enclosure, and illuminated with a convergent beam of intense light entering from one side. Light hitting the colloid particles will be scattered. In discussions about light scattering, the converging beam is called a "Tyndall cone". The scene is viewed through an ordinary microscope placed at right angles to the direction of the lightbeam. Under the microscope, the individual particles will appear as small fuzzy spots of light moving irregularly. The spots are inherently fuzzy because light scattering produces fuzzier images than light reflection. The particles are in Brownian motion in most kinds of liquid and gas colloids, which causes the movement of the spots. The ultramicroscope system can also be used to observe tiny nontransparent particles dispersed in a transparent solid or gel.

Ultramicroscopes have been used for general observation of aerosols and colloids, in studying Brownian motion, in observing ionization tracks in cloud chambers, and in studying biological ultrastructure.

History
In 1902, the ultramicroscope was developed by Richard Adolf Zsigmondy (1865–1929) and Henry Siedentopf (1872–1940), working for Carl Zeiss AG. Applying bright sunlight for illumination they were able to determine the size of 4 nm small nanoparticles in cranberry glass. Zsigmondy further improved the ultramicroscope and presented the immersion ultramicroscope in 1912, allowing the observation of suspended nanoparticles in defined fluidic volumes. In 1925, he was awarded the Nobel Prize in Chemistry for his research on colloids and the ultramicroscope.

Later the development of electron microscopes provided additional ways to see objects too small for light microscopy.

title: Ultramicroscope


text:
Anacoluthon

An anacoluthon (from the Greek anakolouthon, from an- 'not', and akólouthos 'following') is an unexpected discontinuity in the expression of ideas within a sentence, leading to a form of words in which there is logical incoherence of thought. Anacolutha are often sentences interrupted midway, where there is a change in the syntactical structure of the sentence and of intended meaning following the interruption.

An example is the Italian proverb "The good stuff – think about it." This proverb urges people to make the best choice. When anacoluthon occurs unintentionally, it is considered to be an error in sentence structure and may result in incoherent nonsense. However, it can be used intentionally as a rhetorical technique to challenge the reader to think more deeply, or in stream-of-consciousness literature to represent the disjointed nature of associative thought.

Anacolutha are very common in informal speech, where a speaker might start to say one thing, then break off and abruptly and incoherently continue, expressing a completely different line of thought. When such speech is reported in writing, an em dash (—) or ellipsis (...) is often included at the point of discontinuity. The listener is expected to ignore the first part of the sentence, although in some cases it might contribute to the overall meaning in an impressionistic sense.

Examples
"Had ye been there – for what could that have done?"

In Paradise Lost, John Milton uses an anacoluthon with Satan's first words to illustrate his initial confusion:

"If thou beest he; but O how fallen! How changed'"

Additionally, Conrad Aiken's Rimbaud and Verlaine has an extended anacoluthon as it discusses anacoluthon:

Etymology
The word anacoluthon is a transliteration of the Greek ἀνακόλουθον (anakólouthon), which derives from the privative prefix ἀν- an- 'not', and the root adjective ἀκόλουθος akólouthos 'following'. This, incidentally, is precisely the meaning of the Latin phrase non sequitur in logic. However, in classical rhetoric, anacoluthon was used for the logical error of non sequitur and for the syntactic effect or error of changing an expected following or completion to a new or improper one.

Use of the term
The term anacoluthon is used primarily within an academic context. It is most likely to appear in a study of rhetoric or poetry. For example, the 3rd edition of The King's English, a style guide written by H. W. Fowler and F. G. Fowler, mentions it as a major grammatical mistake:

"We can hardly conclude even so desultory a survey of grammatical misdemeanours as this has been without mentioning the most notorious of all. The anacoluthon is a failure to follow on, an unconscious departure from the grammatical scheme with which a sentence was started, the getting switched off, imperceptibly to the writer, very noticeably to his readers, from one syntax track to another."

The word, though not the underlying meaning, has been somewhat popularized due to its use as an expletive by Captain Haddock in the English translations of The Adventures of Tintin series of children's books.

The poet and critic Rachel Blau DuPlessis defines anacoluthon as "the grammatical switching of horses in midstream of a sentence: beginning a sentence in one grammar and ending it in another". She argues that it involves "the employing of multiple discursive ranges and disjunctive transpositions from one to the other[,] hence in any one poem, far from being in one mode, one register, one stable voice, a writer is like an acrobat ... a Barthesean weaver of a wacky fabric, or someone who 'samples', like a certain kind of contemporary DJ".

title: Anacoluthon


text:
Hamina

Hamina (Fredrikshamn,, Sweden ) is a town and a municipality of Finland. It is located approximately 145 km east of the country's capital Helsinki, in the Kymenlaakso region, and formerly the province of Southern Finland. The municipality's population is 0 (as of ) and covers an area of undefined km2, of which undefined km2 is water. The population density is undefined PD/km2. The population of the central town is approximately 10,000. The municipal language of Hamina is Finnish.

Highway 7 (E18) is the town's road connection to Helsinki, after it was upgraded to a continuous motorway in September 2014. Hamina is also the base of one of the most important harbors of Finland, the Port of Hamina-Kotka. The port specializes in forest products and the transit of cargo to Russia. One of Google's five European data centers is situated in Hamina.

History
Vehkalahti was as a municipality first mentioned in 1336. At the proposal of Count Per Brahe, the area surrounding the Vehkalahti church (today St. Mary's Church) received its charter in 1653 through the establishment of Vehkalahden Uusikaupunki (Veckelax Nystad in Swedish, "The New Town of Vehkalahti"). The town was later destroyed during the Great Northern War in 1712. As the commercially vibrant city of Vyborg was lost to Russia in 1721, Fredrikshamn (named in 1723 in the honor of King Frederick I of Sweden) was dedicated to replace it. The town, hitherto a small domestic port with restricted trading privilege's, was granted extensive rights to conduct foreign trade. The Finnish speaking population soon abbreviated the name of the town to Hamina. The reconstruction of the town was completed between 1722 and 1724. The star-shaped fortress and the circular town plan, designed by Axel Löwen, were based on Central European and Italian Renaissance concepts from the 16th century. Fortress towns with a circular street plan like this are quite rare; one example is Palmanova in Italy.

In 1743, Hamina was surrendered to Russia, after the Russo–Swedish War, 1741–1743, and the town of Loviisa was the next Swedish candidate for an Eastern-Finnish trade center. Hamina became a Russian frontier town, for which a fortress was desirable.

The Treaty of Fredrikshamn (1809), by which Sweden ceded Finland, including parts of the province of Lappland and Åland, was signed in Hamina. Thus Sweden was split, and the eastern half was formed into the Grand Duchy of Finland, an autonomous part of the Russian Empire. In 1812, the previously conquered territories known as Old Finland (including Hamina) were joined to the Grand Duchy.

Hamina Cadet School was founded in 1819 and was in operation until 1903. In 1920 the Reserve Officer School began in the same facilities.

Because the town was founded next to the Vehkalahti Church, the municipal center had always been inside the town borders. Vehkalahti and Hamina were consolidated in 2003, and the old coat of arms was replaced with Vehkalahti's coat of arms. The old coat of arms was readopted in January 2013.

Results of the 2021 Finnish municipal elections, resulted in The Finns Party being the largest group on Hamina council, in Hamina.

Main sights

 * Town Hall: Originally built in 1798, it was renovated by Carl Ludvig Engel in 1840.
 * Reserve Officer School: The site which trains reserve officers in the Army Academy of the Finnish Army
 * Town Museum: It is located in a building where King Gustav III of Sweden and Empress Catherine II of Russia met in 1783.
 * Shopkeeper's Museum
 * Google Data Center: (former Stora Enso pulp factory)
 * Hamina Fortress: Built in the 18th century, it is one of the star forts in Finland. The corners of the fortress form six bastions, named after towns in Finland. The Central Bastion was added at the end of the 18th century, and is currently used for cultural events.

Churches

 * St. Mary's Church, previously known as Vehkalahti Church, is the oldest building in Kymenlaakso. It was originally built in the Middle Ages, but it was burnt in 1821 and the current neoclassical exterior is designed by Carl Ludvig Engel and completed in 1828. The church has a museum dedicated to the church life from the 18th century onwards.
 * St. John's Church, formerly known as Hamina Church, was built between 1841-1843. It was designed by Carl Ludvig Engel in the neoclassical style.
 * Church of St. Peter and St. Paul, the Orthodox church in Hamina, was built in 1837. It was designed by Italian-French architect Louis Visconti. The architecture of the church is combination of neoclassical and Byzantine elements.

Twin towns

 * Vordingborg, Denmark
 * Falun, Sweden
 * Paide, Estonia
 * Røros, Norway

Notable people

 * Magnus Enckell (1870–1925), symbolist painter
 * Simo Häyhä (1905–2002), a farmer and military sniper
 * Pelle Miljoona (born 1955), a musician
 * Hugo Simberg (1873–1917), a painter
 * Emilie Mechelin (1838–1917), opera singer and pedagogue
 * Leo Mechelin (1839–1914), a professor, statesman, senator and liberal reformer
 * Keke Rosberg (born 1949), racing driver
 * Meri Toppelius (1863–1896), educational theorist

title: Hamina


text:
Treaty of Fredrikshamn

The Treaty of Fredrikshamn (Freden i Fredrikshamn; Фридрихсгамский мирный договор), or the Treaty of Hamina (Haminan rauha), was a peace treaty concluded between Sweden and Imperial Russia on 17 September 1809. The treaty concluded the Finnish War and was signed in the Finnish town of Hamina (Fredrikshamn). Russia was represented by Nikolay Rumyantsev and David Alopaeus (Russian ambassador to Stockholm), while Sweden by Infantry General Kurt von Stedingk (former Swedish ambassador to Petersburg) and Colonel Anders Fredrik Skjöldebrand.

In the treaty, Sweden ceded Finnish territories to Russia.

Terms
According to the treaty Sweden ceded parts of the provinces Lappland and Västerbotten (east of Tornio River and Muonio River), Åland, and all provinces east thereof. The ceded territories came to constitute the Grand Duchy of Finland, to which also the Russian 18th century conquests of parts of Karelia and Savonia (later to be called Old Finland), were joined in 1812 as Viborg County. Together with the Diet of Porvoo (1809), and the Oath of the Sovereign, the Treaty of Fredrikshamn constitutes the cornerstone for the autonomous Grand Duchy, its own administration and institutions, and thereby a start of the development which would lead to the revival of Finnish culture, to equal position of the Finnish language, and ultimately in 1917 to Finland's independence.

A reference to Emperor Alexander's promise to retain old laws and privileges in Finland was included, but the treaty overstepped any formal guarantees of the legal position of Finland's inhabitants. The Russians refused, and the Swedes were not in a position to insist. Similar clauses had been common in peace treaties, but they were also regularly circumvented. At the period of Russification of Finland, 90 years later, the Russian government argued that the treaty was not violated and hence no outside party had any right to intervene, the question being solely a matter of the Emperor who had granted the original promise.

During the negotiations, Swedish representatives had namely endeavoured to escape the loss of the Åland islands, "the fore-posts of Stockholm," as Napoleon rightly described them. The Åland islands were culturally, ethnically and linguistically purely Swedish, but such facts were of no significance at that time. In the course of the 19th century, it would also turn out that the Åland islands were a British interest, which, after the Crimean War, led to the demilitarization of the islands according to the Åland Convention included in the Treaty of Paris (1856). During the War of the Sixth Coalition, Russia and Sweden concluded an alliance directed against France (5 April 1812). They planned to effect a landing in Swedish Pomerania, which had been overrun by the French. Russia promised to press Denmark into ceding Norway to Sweden. It was understood that Great Britain would join the treaty too, but that never came to pass. Other plans failed to materialise due to Napoleon's invasion of Russia.

title: Treaty of Fredrikshamn


text:
Curry–Howard correspondence

In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.

It is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and the logician William Alvin Howard. It is the link between logic and computation that is usually attributed to Curry and Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various formulations by L. E. J. Brouwer, Arend Heyting and Andrey Kolmogorov (see Brouwer–Heyting–Kolmogorov interpretation) and Stephen Kleene (see Realizability). The relationship has been extended to include category theory as the three-way Curry–Howard–Lambek correspondence.

Origin, scope, and consequences
The beginnings of the Curry–Howard correspondence lie in several observations:
 * 1) In 1934 Curry observes that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic.
 * 2) In 1958 he observes that a certain kind of proof system, referred to as Hilbert-style deduction systems, coincides on some fragment to the typed fragment of a standard model of computation known as combinatory logic.
 * 3) In 1969 Howard observes that another, more "high-level" proof system, referred to as natural deduction, can be directly interpreted in its intuitionistic version as a typed variant of the model of computation known as lambda calculus.

The Curry–Howard correspondence is the observation that there is an isomorphism between the proof systems, and the models of computation. It is the statement that these two families of formalisms can be considered as identical.

If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. 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.

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language. This includes Martin-Löf's intuitionistic type theory and Coquand's Calculus of Constructions, two calculi in which proofs are regular objects of the discourse and in which one can state properties of proofs the same way as of any program. This field of research is usually referred to as modern type theory.

Such typed lambda calculi derived from the Curry–Howard paradigm led to software like Coq in which proofs seen as programs can be formalized, checked, and run.

A converse direction is to use a program to extract a proof, given its correctness—an area of research closely related to proof-carrying code. This is only feasible if the programming language the program is written for is very richly typed: the development of such type systems has been partly motivated by the wish to make the Curry–Howard correspondence practically relevant.

The Curry–Howard correspondence also raised new questions regarding the computational content of proof concepts that were not covered by the original works of Curry and Howard. In particular, classical logic has been shown to correspond to the ability to manipulate the continuation of programs and the symmetry of sequent calculus to express the duality between the two evaluation strategies known as call-by-name and call-by-value.

Because of the possibility of writing non-terminating programs, Turing-complete models of computation (such as languages with arbitrary recursive functions) must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic. The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on using monads to segregate provably terminating from potentially non-terminating code (an approach that also generalizes to much richer models of computation, and is itself related to modal logic by a natural extension of the Curry–Howard isomorphism ). A more radical approach, advocated by total functional programming, is to eliminate unrestricted recursion (and forgo Turing completeness, although still retaining high computational complexity), using more controlled corecursion wherever non-terminating behavior is actually desired.

General formulation
In its more general formulation, the Curry–Howard correspondence is a correspondence between formal proof calculi and type systems for models of computation. In particular, it splits into two correspondences. One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs which, this time, is specific to the particular choice of proof system and model of computation considered.

At the level of formulas and types, the correspondence says that implication behaves the same as a function type, conjunction as a "product" type (this may be called a tuple, a struct, a list, or some other term depending on the language), disjunction as a sum type (this type may be called a union), the false formula as the empty type and the true formula as the unit type (whose sole member is the null object). Quantifiers correspond to dependent function space or products (as appropriate). This is summarized in the following table:

At the level of proof systems and models of computations, the correspondence mainly shows the identity of structure, first, between some particular formulations of systems known as Hilbert-style deduction system and combinatory logic, and, secondly, between some particular formulations of systems known as natural deduction and lambda calculus.

Between the natural deduction system and the lambda calculus there are the following correspondences:

Intuitionistic Hilbert-style deduction systems and typed combinatory logic
It was at the beginning a simple remark in Curry and Feys's 1958 book on combinatory logic: the simplest types for the basic combinators K and S of combinatory logic surprisingly corresponded to the respective axiom schemes α → (β → α) and (α → (β → γ)) → ((α → β) → (α → γ)) used in Hilbert-style deduction systems. For this reason, these schemes are now often called axioms K and S. Examples of programs seen as proofs in a Hilbert-style logic are given below.

If one restricts to the implicational intuitionistic fragment, a simple way to formalize logic in Hilbert's style is as follows. Let Γ be a finite collection of formulas, considered as hypotheses. Then δ is derivable from Γ, denoted Γ ⊢ δ, in the following cases:

 * δ is an hypothesis, i.e. it is a formula of Γ,
 * δ is an instance of an axiom scheme; i.e., under the most common axiom system:
 * δ has the form α → (β → α), or
 * δ has the form (α → (β → γ)) → ((α → β) → (α → γ)),
 * δ follows by deduction, i.e., for some α, both α → δ and α are already derivable from Γ (this is the rule of modus ponens)

This can be formalized using inference rules, as in the left column of the following table.

Typed combinatory logic can be formulated using a similar syntax: let Γ be a finite collection of variables, annotated with their types. A term T (also annotated with its type) will depend on these variables [Γ ⊢ T:δ] when:

 * T is one of the variables in Γ,
 * T is a basic combinator; i.e., under the most common combinator basis:
 * T is K:α → (β → α) [where α and β denote the types of its arguments], or
 * T is S:(α → (β → γ)) → ((α → β) → (α → γ)),
 * T is the composition of two subterms which depend on the variables in Γ.

The generation rules defined here are given in the right-column below. Curry's remark simply states that both columns are in one-to-one correspondence. The restriction of the correspondence to intuitionistic logic means that some classical tautologies, such as Peirce's law ((α → β) → α) → α, are excluded from the correspondence.

Seen at a more abstract level, the correspondence can be restated as shown in the following table. Especially, the deduction theorem specific to Hilbert-style logic matches the process of abstraction elimination of combinatory logic.

Thanks to the correspondence, results from combinatory logic can be transferred to Hilbert-style logic and vice versa. For instance, the notion of reduction of terms in combinatory logic can be transferred to Hilbert-style logic and it provides a way to canonically transform proofs into other proofs of the same statement. One can also transfer the notion of normal terms to a notion of normal proofs, expressing that the hypotheses of the axioms never need to be all detached (since otherwise a simplification can happen).

Conversely, the non provability in intuitionistic logic of Peirce's law can be transferred back to combinatory logic: there is no typed term of combinatory logic that is typable with type
 * ((α → β) → α) → α.

Results on the completeness of some sets of combinators or axioms can also be transferred. For instance, the fact that the combinator X constitutes a one-point basis of (extensional) combinatory logic implies that the single axiom scheme
 * (((α → (β → γ)) → ((α → β) → (α → γ))) → ((δ → (ε → δ)) → ζ)) → ζ,

which is the principal type of X, is an adequate replacement to the combination of the axiom schemes
 * α → (β → α) and
 * (α → (β → γ)) → ((α → β) → (α → γ)).

Intuitionistic Natural deduction and typed lambda calculus
After Curry emphasized the syntactic correspondence between intuitionistic Hilbert-style deduction and typed combinatory logic, Howard made explicit in 1969 a syntactic analogy between the programs of simply typed lambda calculus and the proofs of natural deduction. Below, the left-hand side formalizes intuitionistic implicational natural deduction as a calculus of sequents (the use of sequents is standard in discussions of the Curry–Howard isomorphism as it allows the deduction rules to be stated more cleanly) with implicit weakening and the right-hand side shows the typing rules of lambda calculus. In the left-hand side, Γ, Γ1 and Γ2 denote ordered sequences of formulas while in the right-hand side, they denote sequences of named (i.e., typed) formulas with all names different.

To paraphrase the correspondence, proving Γ ⊢ α means having a program that, given values with the types listed in Γ, manufactures an object of type α. An axiom/hypothesis corresponds to the introduction of a new variable with a new, unconstrained type, the $→ I$ rule corresponds to function abstraction and the $→ E$ rule corresponds to function application. Observe that the correspondence is not exact if the context Γ is taken to be a set of formulas as, e.g., the λ-terms λx.λy.x and λx.λy.y of type $α → α → α$ would not be distinguished in the correspondence. Examples are given below.

Howard showed that the correspondence extends to other connectives of the logic and other constructions of simply typed lambda calculus. Seen at an abstract level, the correspondence can then be summarized as shown in the following table. Especially, it also shows that the notion of normal forms in lambda calculus matches Prawitz's notion of normal deduction in natural deduction, from which it follows that the algorithms for the type inhabitation problem can be turned into algorithms for deciding intuitionistic provability.

Howard's correspondence naturally extends to other extensions of natural deduction and simply typed lambda calculus. Here is a non-exhaustive list:

 * Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus,
 * higher-order logic and Girard's System Fω
 * inductive types as algebraic data type
 * necessity $$\Box$$ in modal logic and staged computation
 * possibility $$\Diamond$$ in modal logic and monadic types for effects
 * The $λ_{I}$ calculus (where abstraction is restricted to λx.E where x has at least one free occurrence in E) and CLI calculus correspond to relevant logic.
 * The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".

Classical logic and control operators
At the time of Curry, and also at the time of Howard, the proofs-as-programs correspondence concerned only intuitionistic logic, i.e. a logic in which, in particular, Peirce's law was not deducible. The extension of the correspondence to Peirce's law and hence to classical logic became clear from the work of Griffin on typing operators that capture the evaluation context of a given program execution so that this evaluation context can be later on reinstalled. The basic Curry–Howard-style correspondence for classical logic is given below. Note the correspondence between the double-negation translation used to map classical proofs to intuitionistic logic and the continuation-passing-style translation used to map lambda terms involving control to pure lambda terms. More particularly, call-by-name continuation-passing-style translations relates to Kolmogorov's double negation translation and call-by-value continuation-passing-style translations relates to a kind of double-negation translation due to Kuroda.

A finer Curry–Howard correspondence exists for classical logic if one defines classical logic not by adding an axiom such as Peirce's law, but by allowing several conclusions in sequents. In the case of classical natural deduction, there exists a proofs-as-programs correspondence with the typed programs of Parigot's λμ-calculus.

Sequent calculus
A proofs-as-programs correspondence can be settled for the formalism known as Gentzen's sequent calculus but it is not a correspondence with a well-defined pre-existing model of computation as it was for Hilbert-style and natural deductions.

Sequent calculus is characterized by the presence of left introduction rules, right introduction rule and a cut rule that can be eliminated. The structure of sequent calculus relates to a calculus whose structure is close to the one of some abstract machines. The informal correspondence is as follows:

The role of de Bruijn
N. G. de Bruijn used the lambda notation for representing proofs of the theorem checker Automath, and represented propositions as "categories" of their proofs. It was in the late 1960s at the same period of time Howard wrote his manuscript; de Bruijn was likely unaware of Howard's work, and stated the correspondence independently (Sørensen & Urzyczyn [1998] 2006, pp 98–99). Some researchers tend to use the term Curry–Howard–de Bruijn correspondence in place of Curry–Howard correspondence.

BHK interpretation
The BHK interpretation interprets intuitionistic proofs as functions but it does not specify the class of functions relevant for the interpretation. If one takes lambda calculus for this class of function, then the BHK interpretation tells the same as Howard's correspondence between natural deduction and lambda calculus.

Realizability
Kleene's recursive realizability splits proofs of intuitionistic arithmetic into the pair of a recursive function and of a proof of a formula expressing that the recursive function "realizes", i.e. correctly instantiates the disjunctions and existential quantifiers of the initial formula so that the formula gets true.

Kreisel's modified realizability applies to intuitionistic higher-order predicate logic and shows that the simply typed lambda term inductively extracted from the proof realizes the initial formula. In the case of propositional logic, it coincides with Howard's statement: the extracted lambda term is the proof itself (seen as an untyped lambda term) and the realizability statement is a paraphrase of the fact that the extracted lambda term has the type that the formula means (seen as a type).

Gödel's dialectica interpretation realizes (an extension of) intuitionistic arithmetic with computable functions. The connection with lambda calculus is unclear, even in the case of natural deduction.

Curry–Howard–Lambek correspondence
Joachim Lambek showed in the early 1970s that the proofs of intuitionistic propositional logic and the combinators of typed combinatory logic share a common equational theory, the theory of cartesian closed categories. The expression Curry–Howard–Lambek correspondence is now used by some people to refer to the relationships between intuitionistic logic, typed lambda calculus and cartesian closed categories, with objects being interpreted as types or propositions and morphisms as terms or proofs. Lambek's correspondence is a correspondence of equational theories, abstracting away from dynamics of computation such as beta reduction and term normalization, and is not the expression of a syntactic identity of structures as it is the case for each of Curry's and Howard's correspondences: i.e. the structure of a well-defined morphism in a cartesian-closed category is not comparable to the structure of a proof of the corresponding judgment in either Hilbert-style logic or natural deduction. For example, it is not possible to state or prove that a morphism is normalizing, establish a Church-Rosser type theorem, or speak of a "strongly normalizing" cartesian closed category. To clarify this distinction, the underlying syntactic structure of cartesian closed categories is rephrased below.

Objects (types) are defined by
 * $$\top$$ is an object
 * if $α$ and $β$ are objects then $$\alpha \times \beta$$ and $$\alpha \rightarrow \beta$$ are objects.

Morphisms (terms) are defined by
 * $$id$$, $$\star$$, $$\operatorname{eval}$$, $$\pi_1$$ and $$\pi_2$$ are morphisms
 * if $t$ is a morphism, λ$t$ is a morphism
 * if $t$ and $u$ are morphisms, $$(t, u)$$ and $$u \circ t$$ are morphisms.

Well-defined morphisms (typed terms) are defined by the following typing rules (in which the usual categorical morphism notation $$f : \alpha \to \beta$$ is replaced with sequent calculus notation $$f :\!\!- \alpha ~\vdash~ \beta$$).

Identity:
 * $$\frac{}{id:\!\!- \alpha ~\vdash~ \alpha}$$

Composition:
 * $$\frac{t:\!\!- \alpha ~\vdash~ \beta\qquad u:\!\!- \beta ~\vdash~ \gamma}{u \circ t:\!\!- ~\alpha ~\vdash~ \gamma}$$

Unit type (terminal object):
 * $$\frac{}{\star:\!\!-\alpha ~\vdash~ \top}$$

Cartesian product:
 * $$\frac{t:\!\!-\alpha ~\vdash~ \beta\qquad u:\!\!-\alpha ~\vdash~ \gamma}{(t,u):\!\!- \alpha ~\vdash~ \beta \times \gamma}$$

Left and right projection:
 * $$\frac{}{\pi_1:\!\!- \alpha \times \beta ~\vdash~ \alpha}\qquad\frac{}{\pi_2:\!\!- \alpha \times \beta ~\vdash~ \beta}$$

Currying:
 * $$\frac{t:\!\!- \alpha \times \beta ~\vdash~ \gamma}{\lambda t:\!\!- \alpha ~\vdash~ \beta \rightarrow \gamma}$$

Application:
 * $$\frac{}{eval:\!\!- (\alpha \rightarrow \beta) \times \alpha ~\vdash~ \beta}$$

Finally, the equations of the category are
 * $$id \circ t = t$$
 * $$t \circ id = t$$
 * $$(v \circ u) \circ t = v \circ (u \circ t)$$
 * $$\star = id$$ (if well-typed)
 * $$\star \circ u = \star$$
 * $$\pi_1 \circ (t, u) = t$$
 * $$\pi_2 \circ (t,u) = u$$
 * $$(\pi_1, \pi_2) = id$$
 * $$(t_1, t_2) \circ u = (t_1 \circ u, t_2 \circ u) $$
 * $$eval \circ (\lambda t \circ \pi_1, \pi_2) = t$$
 * $$\lambda eval = id$$
 * $$\lambda t \circ u = \lambda (t \circ (u \circ \pi_1, \pi_2))$$

These equations imply the following $$\eta$$-laws:
 * $$(\pi_1 \circ t, \pi_2 \circ t) = t$$
 * $$\lambda (eval \circ (t \circ \pi_1, \pi_2)) = t$$

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.

Examples
Thanks to the Curry–Howard correspondence, a typed expression whose type corresponds to a logical formula is analogous to a proof of that formula. Here are examples.

The identity combinator seen as a proof of α → α in Hilbert-style logic
As an example, consider a proof of the theorem $α → α$. In lambda calculus, this is the type of the identity function $I = λx.x$ and in combinatory logic, the identity function is obtained by applying S = λfgx.fx(gx) twice to K = λxy.x. That is, $I = ((S K) K)$. As a description of a proof, this says that the following steps can be used to prove $α → α$:

 * instantiate the second axiom scheme with the formulas $α$, $β → α$ and $α$ to obtain a proof of $(α → ((β → α) → α)) → ((α → (β → α)) → (α → α))$,
 * instantiate the first axiom scheme once with $α$ and $β → α$ to obtain a proof of $α → ((β → α) → α)$,
 * instantiate the first axiom scheme a second time with $α$ and $β$ to obtain a proof of $α → (β → α)$,
 * apply modus ponens twice to obtain a proof of $α → α$

In general, the procedure is that whenever the program contains an application of the form (P Q), these steps should be followed:
 * 1) First prove theorems corresponding to the types of P and Q.
 * 2) Since P is being applied to Q, the type of P must have the form $α → β$ and the type of Q must have the form $α$ for some $α$ and $β$. Therefore, it is possible to detach the conclusion, $β$, via the modus ponens rule.

The composition combinator seen as a proof of (β → α) → (γ → β) → γ → α in Hilbert-style logic
As a more complicated example, let's look at the theorem that corresponds to the B function. The type of B is $(β → α) → (γ → β) → γ → α$. B is equivalent to (S (K S) K). This is our roadmap for the proof of the theorem $(β → α) → (γ → β) → γ → α$.

The first step is to construct (K S). To make the antecedent of the K axiom look like the S axiom, set $α$ equal to $(α → β → γ) → (α → β) → α → γ$, and $β$ equal to $δ$ (to avoid variable collisions):

Since the antecedent here is just S, the consequent can be detached using Modus Ponens:

This is the theorem that corresponds to the type of (K S). Now apply S to this expression. Taking S as follows

put $K : α → β → α$, $K[α = (α → β → γ) → (α → β) → α → γ, β = δ] : ((α → β → γ) → (α → β) → α → γ) → δ → (α → β → γ) → (α → β) → α → γ$, and $K S : δ → (α → β → γ) → (α → β) → α → γ$, yielding

and then detach the consequent:

This is the formula for the type of (S (K S)). A special case of this theorem has $S : (α → β → γ) → (α → β) → α → γ$:

This last formula must be applied to K. Specialize K again, this time by replacing $α = δ$ with $β = α → β → γ$ and $γ = (α → β) → α → γ$ with $S[α = δ, β = α → β → γ, γ = (α → β) → α → γ] : (δ → (α → β → γ) → (α → β) → α → γ) → (δ → (α → β → γ)) → δ → (α → β) → α → γ$:

This is the same as the antecedent of the prior formula so, detaching the consequent:

Switching the names of the variables $S (K S) : (δ → α → β → γ) → δ → (α → β) → α → γ$ and $δ = (β → γ)$ gives us

which was what remained to prove.

The normal proof of (β → α) → (γ → β) → γ → α in natural deduction seen as a λ-term
The diagram below gives proof of $S (K S)[δ = β → γ] : ((β → γ) → α → β → γ) → (β → γ) → (α → β) → α → γ$ in natural deduction and shows how it can be interpreted as the λ-expression $α$ of type $(β → γ)$.

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) : (β → α) → (γ → β) → γ → α

Other applications
Recently, the isomorphism has been proposed as a way to define search space partition in genetic programming. The method indexes sets of genotypes (the program trees evolved by the GP system) by their Curry–Howard isomorphic proof (referred to as a species).

As noted by INRIA research director Bernard Lang, the Curry-Howard correspondence constitutes an argument against the patentability of software: since algorithms are mathematical proofs, patentability of the former would imply patentability of the latter. A theorem could be private property; a mathematician would have to pay for using it, and to trust the company that sells it but keeps its proof secret and rejects responsibility for any errors.

Generalizations
The correspondences listed here go much farther and deeper. For example, cartesian closed categories are generalized by closed monoidal categories. The internal language of these categories is the linear type system (corresponding to linear logic), which generalizes simply-typed lambda calculus as the internal language of cartesian closed categories. Moreover, these can be shown to correspond to cobordisms, which play a vital role in string theory.

An extended set of equivalences is also explored in homotopy type theory. Here, type theory is extended by the univalence axiom ("equivalence is equivalent to equality") which permits homotopy type theory to be used as a foundation for all of mathematics (including set theory and classical logic, providing new ways to discuss the axiom of choice and many other things). That is, the Curry–Howard correspondence that proofs are elements of inhabited types is generalized to the notion of homotopic equivalence of proofs (as paths in space, the identity type or equality type of type theory being interpreted as a path).

Seminal references

 * De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag, 1983, pp. 159–200.
 * De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag, 1983, pp. 159–200.
 * De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967–1970, Springer Verlag, 1983, pp. 159–200.

Extensions of the correspondence

 * . (Full version of the paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139–1140, 1991.)
 * . (Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753–754, 1993.)
 * . (Full version of a paper presented at 2nd WoLLIC'95, Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
 * , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
 * . (Full version of a paper presented at LSFA 2010, Natal, Brazil.)
 * . (Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753–754, 1993.)
 * . (Full version of a paper presented at 2nd WoLLIC'95, Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330–332, 1996.)
 * , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
 * . (Full version of a paper presented at LSFA 2010, Natal, Brazil.)
 * , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
 * . (Full version of a paper presented at LSFA 2010, Natal, Brazil.)

Philosophical interpretations

 * . (Early version presented at Logic Colloquium '88, Padova. Abstract in JSL 55:425, 1990.)
 * . (Early version presented at Fourteenth International Wittgenstein Symposium (Centenary Celebration) held in Kirchberg/Wechsel, August 13–20, 1989.)

Synthetic papers

 * , the contribution of de Bruijn by himself.
 * , contains a synthetic introduction to the Curry–Howard correspondence.
 * , contains a synthetic introduction to the Curry–Howard correspondence.

Books

 * , reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
 * , notes on proof theory and type theory, that includes a presentation of the Curry–Howard correspondence, with a focus on the formulae-as-types correspondence
 * , notes on proof theory with a presentation of the Curry–Howard correspondence.
 * , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.
 * , concerns the adaptation of proofs-as-programs program synthesis to coarse-grain and imperative program development problems, via a method the authors call the Curry–Howard protocol. Includes a discussion of the Curry–Howard correspondence from a Computer Science perspective.

title: Curry–Howard correspondence


text:
Yoo-hoo

Yoo-hoo is an American brand of chocolate-flavored beverage that was created by Natale Olivieri in Garfield, New Jersey, in 1928 and is currently manufactured by Keurig Dr Pepper. As of 2019, the drink is primarily made from water, high-fructose corn syrup and whey.

History
Yoo-hoo was created in Garfield, New Jersey, in 1928 by Natale Olivieri, who had been bottling carbonated fruit drinks.

In the 1940s, Thomas Giresi opened a bottling plant in Batesburg, South Carolina, for distribution of Yoo-hoo. In the 1960s, an advertising campaign tried to appeal to an older public for the drink, and featured Yogi Berra and his New York Yankees teammates. Berra, in a pin-striped business suit, drinks a bottle of Yoo-hoo, lifts it next to his cheek, and says with a smile, "It's Me-He for Yoo-Hoo!"

Later, Yoo-hoo advertised as : Yoo-hoo, the chocolate action drink.

BBC Industries purchased the rights to Yoo-hoo sometime in the 1950s and retained ownership until 1976, when it sold the brand to Iroquois Brands. Yoo-hoo was sold again in 1981 to a group of private investors, which owned the brand until 1989, when it was sold to the French conglomerate Pernod Ricard.

In 2001, Pernod Ricard sold Yoo-hoo to Cadbury Schweppes, with production responsibilities falling to CS's Mott's group and marketing and advertising responsibilities under Snapple. They heightened awareness of the once-popular beverage.

The drink company's headquarters are in Tarrytown, New York, with plants in Carlstadt, New Jersey, and Aspers, Pennsylvania. An Opelousas, Louisiana, location closed in 2009. At one time, Yoo-hoo owned several other chocolate milk brands as well, including Choc-Ola, Brownie, Cocoa Dusty, and Chocolate Soldier.

In May 2008, Cadbury-Schweppes split into the Cadbury candy business and the Dr Pepper Snapple Group soft drink firm, with the latter taking over Yoo-hoo.

Alleged misleading advertising
In 2010, a legal suit was brought against the Dr Pepper Snapple Group in New York state by Timothy Dahl. The suit alleged that the Dr Pepper Snapple Group engaged in misleading advertising as to nutritional makeup of Yoo-hoo. Papers filed by Dahl claimed that the drink "contains dangerous, unhealthy, non-nutritious partially hydrogenated oil". Further, he stated that the drink "contains virtually no milk and instead is mostly water, sugars, milk by-products and chemicals." However, Motts LLP, which made the drink during this time said the drink contains "seven vitamins and minerals and no preservatives" and they stood by their product.

Flavors
Yoo-hoo began introducing new flavors to its lineup in 1995, including chocolate-coconut, chocolate-mint, chocolate-banana, and chocolate-strawberry. Yoo-hoo's other flavors have included vanilla, strawberry, cookies & cream, chocolate peanut butter, and chocolate caramel. The Double Fudge, banana, and Island Coconut flavors were discontinued.

title: Yoo-hoo


text:
Talk:Eugeen Van Mieghem

Untitled
If you have any comment on my text, please let me know Erwin Joos, curator Van Mieghem Museum

 * Do you know of any books or websites that show Van Mieghem's work? I would like to add a "References" section to the article. -- Heron

Have a look on Wolseley Fine Arts London, the Van Mieghem Museum is working on a web-site Regards, Erwin Joos

title: Talk:Eugeen Van Mieghem


text:
Xylometazoline

Xylometazoline, also spelled xylomethazoline, is a medication used to reduce symptoms of nasal congestion, allergic rhinitis, and sinusitis. Use is not recommended for more than seven days. Use is also not recommended in those less than three months of age and some say not less than 6 years of age. It is used directly in the nose as a spray or drops.

Side effects include trouble sleeping, irritation of the nose, nausea, nosebleed (3%), period pain (10%) and headache (3%). Long term use (> 10 days) is not recommended due to a rhinitis medicamentosa when stopped. Use is not recommended during pregnancy. Xylometazoline is in the decongestant and alpha-adrenergic agonist families of medication.

One study classified it with selectivity ratios in alpha 2 adrenergic receptors of 151 for a2A vs a2B, 4.5 a2A vs a2C, and 33.9 a2B vs a2C. Making it a highly selective a2A agonist.

Xylometazoline was patented in 1956 and came into medical use in 1959. It is on the World Health Organization's List of Essential Medicines. Xylometazoline is available as a generic medication.

Mechanism of action
The drug works by stimulating adrenergic receptors on the lamina propria of blood vessels in the nose. The decongestant effect is due to constriction of large veins in the nose which swell up during the inflammation of any infection or allergy of the nose. The smaller arteries are also constricted and this causes the colour of the nasal epithelium to be visibly paler after dosage.

Xylometazoline is an imidazole derivative which is designed to mimic the molecular shape of adrenaline. It binds to α1 and α2 adrenergic receptors in the nasal mucosa. Due to its sympathomimetic effects, it should not be used by people with high blood pressure, or other heart problems.

Extended usage of xylometazoline can result in decreased effectiveness or a buildup of tolerance against the drug. The number of receptors decreases, and when the administration of the drug is ceased, chronic congestion can occur; this is called rhinitis medicamentosa, commonly referred to as rebound congestion. Moreover, long-term overdosing can cause degenerative changes in nasal mucous membranes that pose another health problem.

Brand names
The most common name for over-the-counter products containing xylometazoline internationally is "Otrivin" (used in Australia, Canada, Estonia, Finland, Greece, Hungary, India, Israel, Jordan, Netherlands, New Zealand, Norway, Poland, South Africa, Sweden, Vietnam, Hong Kong), "Otrivine" (United Kingdom, Ireland, Turkey, Belgium), or "Otriven" (Germany). A product marketed as "Otrivin Oxy" contains oxymetazoline instead of xylometazoline.

Other product names used include Antazol (Square, in Bangladesh), Xylomet (Opsonin, Bangladesh), Cirovin, Klarigen (in Denmark), Nasolin, Neo-Rinoleina, Novorin, Olynth, Otrinoz, Galazolin (Russia, Ukraine, Belarus), Nasomist-X, Otrix, Rhinoset, Zenfresh, Naphthyzinium, Xymelyn (in Latvia), Sinutab Nasal Spray, Snup akut, Sudafed, Xylo-COMOD, Xylolin (in the United Arab Emirates), Xylovit, Olynth (in Serbia, the Czech Republic and Slovakia), Meralys (in Croatia) Xynosine (in Pakistan, Afghanistan, Kyrgyzstan and Kazakhstan), Xymelin, Zymelin, Xylostar, Xylorin (in Poland), Nasobol, Xylo Mepha and others (Switzerland), Decozal (in Jordan), Nasic, Orinox (Romania), Narhimed (Italy), nasa Rhinathiol (Belgium) and Zolinol, Nasorhinathiol and Vibrocil (Portugal].

As of 2021, a number of consumer products containing xylometazoline are marketed in the United States.

Formulations
The standard adult solution strength is 0.1% w/v xylometazoline (or 1 mg per 1 mL solution), and the dose for children under 12 is usually 0.05% (0.5 mg/mL).

title: Xylometazoline